lt_gamma0 — Mathlib

English

Γ₀ is the limit of the iterates of the function a ↦ veblen(a, 0).

Русский

Γ₀ есть предел последовательности, полученной итерацией функции a ↦ veblen(a, 0).

LaTeX

$$$o < Γ_0 \iff \exists n : \mathbb{N}, o < (\lambda a. \\veblen(a,0))^{[n]} 0$$$

Lean4

/-- `Γ₀` is the limit of `0`, `veblen 0 0`, `veblen (veblen 0 0) 0`, … -/
theorem lt_gamma0 : o < Γ₀ ↔ ∃ n : ℕ, o < (fun a ↦ veblen a 0)^[n] 0 := by rw [gamma0_eq_nfp, lt_nfp_iff]

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