Documentation

Lean 4 Proof

theorem lower_rho_more_averse {ρ₁ ρ₂ : ℝ} (h : ρ₁ < ρ₂) :
    inequalityAversion ρ₂ < inequalityAversion ρ₁ := by
  simp only [inequalityAversion]; linarith

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/SocialWelfare.lean:78

Module Section

CES as Atkinson Social Welfare Function

In the same file