Theorem Ordinal.isCofinal_setOfPred_isInitial

Modification history

2026-10-10 11:48
Mathlib/SetTheory/Cardinal/Aleph.lean
chore: redefine `Ordinal.preOmega` using `Order.enum` (#39847) …
Added Ordinal.isCofinal_setOfPred_isInitialView on Github →