Theorem Order.cof_cardinal

Modification history

2026-05-25 09:15
Mathlib/SetTheory/Cardinal/Aleph.lean
feat: cofinal subset of regular cardinal is isomorphic to it (#38362) …
Modified Order.cof_cardinalView on Github →
2026-05-10 20:52
Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean
feat: `Order.cof Ordinal = univ` (#37675)
Added Order.cof_cardinalView on Github →