Documentation

Lean 4 Proof

theorem saezTopRate_lt_one {a e : ℝ} (ha : 0 < a) (he : 0 < e) :
    saezTopRate a e < 1 := by
  simp only [saezTopRate]
  rw [div_lt_one (by nlinarith : (0:ℝ) < 1 + a * e)]
  nlinarith

Dependency Graph

Location

thesis/CESProofs/Macro/TaxStructure.lean:310

Module Section

Government Tax Structure (Layer 3 of Macro Extension)

In the same file