Theorem Cardinal.succ_preAleph

Modification history

2026-03-30 08:57
Mathlib/SetTheory/Cardinal/Aleph.lean
feat: cof (ω_ (o + 1)) = ℵ_ (o + 1) (#37020)
Added Cardinal.succ_preAlephView on Github →