Theorem Ordinal.cof_omega0

Modification history

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 →