lt_epsilon0 — Mathlib

English

For every ordinal o, o < ε₀ if and only if there exists n ∈ ℕ with o < (ω^a)^[n] 0.

Русский

Для каждого ординала o справедливо: o < ε₀ тогда и только тогда, когда существует n ∈ ℕ такое, что o < (ω^a)^[n] 0.

LaTeX

$$$o < \varepsilon_0 \iff \exists n:\; o < (\lambda a. ω^a)^{[n]} 0$$$

Lean4

/-- `ε₀` is the limit of `0`, `ω ^ 0`, `ω ^ ω ^ 0`, … -/
theorem lt_epsilon0 : o < ε₀ ↔ ∃ n : ℕ, o < (fun a ↦ ω ^ a)^[n] 0 := by rw [epsilon0_eq_nfp, lt_nfp_iff]

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