Documentation

Lean 4 Proof

theorem saezTopRate_pos {a e : ℝ} (_ha : 0 < a) (_he : 0 < e) :
    0 < saezTopRate a e := by
  simp only [saezTopRate]
  exact div_pos one_pos (by nlinarith)

Dependency Graph

Location

thesis/CESProofs/Macro/TaxStructure.lean:304

Module Section

Government Tax Structure (Layer 3 of Macro Extension)

In the same file