Theorem Cardinal.aleph_one_lt_lift

Modification history

2025-12-22 18:39
Mathlib/SetTheory/Cardinal/Aleph.lean
refactor: standardize spelling of `ℵ₁` as `aleph_one` (#33198) …
Added Cardinal.aleph_one_lt_liftView on Github →