Theorem Ordinal.iSup_lt_omega_one

Modification history

2026-04-05 15:16
Mathlib/SetTheory/Cardinal/Regular.lean
feat: supremum of countably many countable ordinals is countable (#37025) …
Added Ordinal.iSup_lt_omega_oneView on Github →