Theorem Ordinal.exists_ord_cof_eq

Modification history

2026-06-03 11:16
Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean
feat: a cofinal set has a cofinal subset of order type `(cof α).ord` (#39789)
Modified Ordinal.exists_ord_cof_eqView on Github →
2026-05-25 23:43
Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean
chore: rename `Order.cof_eq` → `Order.exists_cof_eq` (#39851)
Added Ordinal.exists_ord_cof_eqView on Github →