iterate_veblen_lt_gamma0 — Mathlib

English

For every n, the n-th iterate of the map a ↦ veblen(a, 0) at 0 is below Γ₀.

Русский

Для каждого n последовательность (veblen a 0)^[n] 0 меньше Γ₀.

LaTeX

$$$( \\lambda a. \\veblen(a,0) )^{[n]} 0 < Γ_0$$$

Lean4

/-- `veblen (veblen … (veblen 0 0) … 0) 0 < Γ₀` -/
theorem iterate_veblen_lt_gamma0 (n : ℕ) : (fun a ↦ veblen a 0)^[n] 0 < Γ₀ :=
  by
  rw [gamma0_eq_nfp]
  apply iterate_lt_nfp veblen_zero_strictMono
  simp

Похожие утверждения