Documentation

Lean 4 Proof

theorem taxRevenue_increasing_in_τcorp {τ_L τ_K τ_C τ_corp₁ τ_corp₂ wL rK C Prof : ℝ}
    (hProf : 0 < Prof) (hτ : τ_corp₁ < τ_corp₂) :
    taxRevenue τ_L τ_K τ_C τ_corp₁ wL rK C Prof <
    taxRevenue τ_L τ_K τ_C τ_corp₂ wL rK C Prof := by
  simp only [taxRevenue]; nlinarith

Dependency Graph

Location

thesis/CESProofs/Macro/TaxStructure.lean:143

Module Section

Government Tax Structure (Layer 3 of Macro Extension)

In the same file