isInitial_succ — Mathlib

English

For any ordinal o, the successor of o is initial if and only if o is less than ω.

Русский

Для любого ординала o переход к следующему после o начальный тогда и только тогда, когда o < ω.

LaTeX

$$$\mathrm{IsInitial}(\operatorname{succ}(o)) \iff o < \omega$$$

Lean4

theorem isInitial_succ {o : Ordinal} : IsInitial (succ o) ↔ o < ω :=
  ⟨Function.mtr fun hwo ↦ ne_of_lt <| by simp_all [ord_card_le], fun how ↦
    (Ordinal.lt_omega0.1 how).rec fun n h ↦ h ▸ isInitial_natCast (n + 1)⟩

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