Theorem Ordinal.cof_eq_aleph0_of_isSuccLimit

Modification history

2026-03-27 17:02
Mathlib/SetTheory/Cardinal/Cofinality.lean
feat: countable limit ordinal has cofinality ℵ₀ (#37029)
Added Ordinal.cof_eq_aleph0_of_isSuccLimitView on Github →