English
If c is an infinite cardinal, ord(c) is a succ-limit ordinal.
Русский
Если c бесконечный кардинал, ord(c) является предельным ординалом.
LaTeX
$$$\forall c\; (\aleph_0 \le c) \to IsSuccLimit(\operatorname{ord}(c))$$$
Lean4
theorem isSuccLimit_ord {c} (co : ℵ₀ ≤ c) : IsSuccLimit (ord c) :=
by
rw [isSuccLimit_iff, isSuccPrelimit_iff_succ_lt]
refine ⟨fun h => aleph0_ne_zero ?_, fun a => lt_imp_lt_of_le_imp_le fun h => ?_⟩
· rw [← Ordinal.le_zero, ord_le] at h
simpa only [card_zero, nonpos_iff_eq_zero] using co.trans h
· rw [ord_le] at h ⊢
rwa [← @add_one_of_aleph0_le (card a), ← card_succ]
rw [← ord_le, ← IsSuccLimit.le_succ_iff, ord_le]
· exact co.trans h
· rw [ord_aleph0]
exact Ordinal.isSuccLimit_omega0
