Commit 2026-04-05 15:16 8910a139
View on Github →feat: supremum of countably many countable ordinals is countable (#37025) This theorem already existed, but we clean it up by using ω₁ and generalize its universes.
feat: supremum of countably many countable ordinals is countable (#37025) This theorem already existed, but we clean it up by using ω₁ and generalize its universes.