Commit 2025-02-13 14:43 2278a542
View on Github →feat(SetTheory): regular cardinals have a least element (#21780)
Ordinal.toTypeOrderBotOfPos
is deprecated in favour of a new definition Ordinal.toTypeOrderBotOfPos
which takes an assumption o ≠ 0
. A similar definition is introduced for cardinals, and a lemma Cardinal.IsRegular.ne_zero
is added. As a result, if c
is a regular cardinal, then c.ord.toType
has a least element.