Theorem Order.type_eq_of_isCofinal

Modification history

2026-05-25 09:15
Mathlib/SetTheory/Cardinal/Cofinality/Enum.lean
feat: cofinal subset of regular cardinal is isomorphic to it (#38362) …
Added Order.type_eq_of_isCofinalView on Github →