Theorem Ordinal.cof_preOmega

Modification history

2024-12-14 15:31

Mathlib/SetTheory/Cardinal/Cofinality.lean

feat(SetTheory/Cardinal/Cofinality): generalize `cof_preOmega` (#19916) …

Modified Ordinal.cof_preOmega View on Github →

2024-11-01 19:53

Mathlib/SetTheory/Cardinal/Cofinality.lean

feat(SetTheory/Cardinal/Aleph): simpler definition of `aleph` (#17674) …

Added Ordinal.cof_preOmega View on Github →