Theorem Ordinal.iSup_sequence_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) …
Deleted Ordinal.iSup_sequence_lt_omega_oneView on Github →
2025-12-22 18:39
Mathlib/SetTheory/Cardinal/Regular.lean
refactor: standardize spelling of `ℵ₁` as `aleph_one` (#33198) …
Added Ordinal.iSup_sequence_lt_omega_oneView on Github →