apply_of_isSuccLimit — Mathlib

English

If f is normal and o is a succ-limit ordinal, then f(o) equals the supremum over all a < o of f(a).

Русский

Если f нормальная, а o — succ-пределенный ординал, то f(o) равен верхней границе по a < o от f(a).

LaTeX

$$$$ f(o) = \\sup_{a < o} f(a) $$$$

Lean4

theorem apply_of_isSuccLimit {f : Ordinal.{u} → Ordinal.{v}} (H : IsNormal f) {o : Ordinal} (ho : IsSuccLimit o) :
    f o = ⨆ a : Iio o, f a := by
  have : Nonempty (Iio o) := ⟨0, ho.bot_lt⟩
  rw [← H.map_iSup, ho.iSup_Iio]

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