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.

Estimated changes