Theorem Order.enum_succ_le_of_lt

Modification history

2026-07-03 00:00
Mathlib/SetTheory/Cardinal/Cofinality/Enum.lean
feat: more results on `Order.enum` (#39136) …
Modified Order.enum_succ_le_of_ltView on Github →
2026-05-25 09:15
Mathlib/SetTheory/Cardinal/Cofinality/Enum.lean
feat: cofinal subset of regular cardinal is isomorphic to it (#38362) …
Added Order.enum_succ_le_of_ltView on Github →