Documentation

Lean 4 Proof

theorem welfareDistanceFn_pos {z : ℝ} (hz : 0 < z) (hne : z ≠ 1) :
    0 < welfareDistanceFn z := by
  have hge := welfareDistanceFn_nonneg hz
  exact lt_of_le_of_ne hge (Ne.symm (mt (welfareDistanceFn_eq_zero_iff hz).mp hne))

Dependency Graph

Location

thesis/CESProofs/Hierarchy/WelfareDecomposition.lean:261

Module Section

Theorems 7-8, Propositions 5 and 7, Corollary 3:

In the same file