apply_omega0 — Mathlib

English

For any normal function f, the supremum of f over natural numbers equals f(ω0).

Русский

Для любой нормальной функции f верхняя граница значений f на натуральных равна f(ω0).

LaTeX

$$$\\forall f\\ (hf : IsNormal\\ f),\\; \\big\\langle \\sup_{n\\in\\mathbb{N}} f(n) \\big\\rangle = f(\\omega_0)$$$

Lean4

theorem apply_omega0 {f : Ordinal.{u} → Ordinal.{v}} (hf : IsNormal f) : ⨆ n : ℕ, f n = f ω := by
  rw [← iSup_natCast, hf.map_iSup]

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