Documentation

Lean 4 Proof

theorem corporateProfit_pos {Y Jσ : ℝ} (hY : 0 < Y) (hJσ : 0 < Jσ) :
    0 < corporateProfit Y Jσ := by
  simp only [corporateProfit]; exact div_pos hY hJσ

Dependency Graph

Location

thesis/CESProofs/Macro/TaxStructure.lean:154

Module Section

Government Tax Structure (Layer 3 of Macro Extension)

In the same file