Theorem Cardinal.lift_lt_aleph_one

Modification history

2026-10-10 09:42
Mathlib/SetTheory/Cardinal/Aleph.lean
chore: delete deprecated declarations to March 2026 (#44240)
Deleted Cardinal.lift_lt_aleph_oneView on Github →
2026-04-05 15:16
Mathlib/SetTheory/Cardinal/Aleph.lean
feat: many simp lemmas about aleph/beth/omega functions and lift (#37363)
Modified Cardinal.lift_lt_aleph_oneView on Github →
2025-12-22 18:39
Mathlib/SetTheory/Cardinal/Aleph.lean
refactor: standardize spelling of `ℵ₁` as `aleph_one` (#33198) …
Added Cardinal.lift_lt_aleph_oneView on Github →