Documentation

Lean 4 Proof

theorem corporateProfit_decreasing_in_Jσ {Y Jσ₁ Jσ₂ : ℝ} (hY : 0 < Y)
    (hJσ₁ : 0 < Jσ₁) (_hJσ₂ : 0 < Jσ₂) (hJσ : Jσ₁ < Jσ₂) :
    corporateProfit Y Jσ₂ < corporateProfit Y Jσ₁ := by
  simp only [corporateProfit]
  exact div_lt_div_of_pos_left hY hJσ₁ hJσ

Dependency Graph

Location

thesis/CESProofs/Macro/TaxStructure.lean:169

Module Section

Government Tax Structure (Layer 3 of Macro Extension)

In the same file