Theorem Ordinal.exists_ord_cof_eq_of_isCofinal

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)
Added Ordinal.exists_ord_cof_eq_of_isCofinalView on Github →