epsilon_succ_eq_nfp — Mathlib

English

For any ordinal o, the epsilon number at succ(o) equals the fixed point iteration of the successor applied to ε_o: ε_(succ o) = nfp (ω^a) (succ (ε_o)).

Русский

Для любого ординала o, ε_(succ o) равняется итерации фиксированной точки для ω^a, применённой к succ(ε_o): ε_(succ o) = nfp (ω^a) (succ (ε_o)).

LaTeX

$$$\varepsilon_{(\mathrm{succ} o)} = nfp(\lambda a. ω^a)(\mathrm{succ}(\varepsilon_o))$$$

Lean4

theorem epsilon_succ_eq_nfp (o : Ordinal) : ε_ (succ o) = nfp (fun a ↦ ω ^ a) (succ (ε_ o)) := by
  rw [epsilon_eq_deriv, epsilon_eq_deriv, deriv_succ]

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