Theorem Order.cof_eq_aleph0

Modification history

2026-05-10 00:45
Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean
chore: split `SetTheory.Cardinal.Cofinality` (#38363) …
Modified Order.cof_eq_aleph0View on Github →
2026-03-27 17:02
Mathlib/SetTheory/Cardinal/Cofinality.lean
feat: countable limit ordinal has cofinality ℵ₀ (#37029)
Added Order.cof_eq_aleph0View on Github →