Commit 2024-12-14 15:31 b8d06210

View on Github →

feat(SetTheory/Cardinal/Cofinality): generalize cof_preOmega (#19916) This lemma is also true for o = 0, so we can take a IsSuccPrelimit argument instead of an IsLimit argument.

Estimated changes

modified theorem Ordinal.cof_preOmega