Documentation

Lean 4 Proof

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

Dependency Graph

Location

thesis/CESProofs/Macro/TaxStructure.lean:159

Module Section

Government Tax Structure (Layer 3 of Macro Extension)

In the same file