Documentation

Lean 4 Proof

theorem saezTopRate_decreasing_in_e {a e₁ e₂ : ℝ}
    (_ha : 0 < a) (_he₁ : 0 < e₁) (_he₂ : 0 < e₂) (he : e₁ < e₂) :
    saezTopRate a e₂ < saezTopRate a e₁ := by
  simp only [saezTopRate]
  exact div_lt_div_of_pos_left one_pos (by nlinarith) (by nlinarith)

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/TaxStructure.lean:318

Module Section

Government Tax Structure (Layer 3 of Macro Extension)

In the same file