Theorem Ordinal.cof_omega0

Modification history

2026-03-27 17:02
Mathlib/SetTheory/Cardinal/Cofinality.lean
feat: countable limit ordinal has cofinality ℵ₀ (#37029)
Modified Ordinal.cof_omega0View on Github →
2026-03-23 01:32
Mathlib/SetTheory/Cardinal/Cofinality.lean
feat: cof α < ℵ₀ ↔ cof α ≤ 1 (#36976)
Modified Ordinal.cof_omega0View on Github →
2024-10-03 10:05
Mathlib/SetTheory/Cardinal/Cofinality.lean
refactor(SetTheory/Ordinal/Basic): deprecate Ordinal.omega in favor of Ordinal.omega0 (#17158) …
Added Ordinal.cof_omega0View on Github →