Documentation

Lean 4 Proof

theorem concentration_compounds {N : ℕ} {T : ℕ} (hN : 2 ≤ N) (hT : 0 < T) :
    1 < (↑N : ℝ) ^ T := by
  have hNgt1 : (1 : ℝ) < ↑N := by exact_mod_cast (by omega : 1 < N)
  exact one_lt_pow₀ hNgt1 hT.ne'

Dependency Graph

Location

thesis/CESProofs/Applications/FairInheritance.lean:295

Module Section

Fair Inheritance: Taxing Concentration, Not Transfer

In the same file