Theorem Order.cof_eq_of_isCofinal

Modification history

2026-06-03 11:16
Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean
feat: a cofinal set has a cofinal subset of order type `(cof α).ord` (#39789)
Added Order.cof_eq_of_isCofinalView on Github →