Commit 2024-10-22 14:15 9a2abc12

View on Github →

feat(SetTheory/Cardinal/Basic): lift (aleph' o) = aleph' (lift o) (#16306) plus some lemmas on ℵ₁ and lift.

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Aleph.lean

added theorem Cardinal.aleph1_eq_lift

added theorem Cardinal.aleph1_le_lift

added theorem Cardinal.aleph1_lt_lift

added theorem Cardinal.lift_aleph'

added theorem Cardinal.lift_aleph

added theorem Cardinal.lift_eq_aleph1

added theorem Cardinal.lift_le_aleph1

added theorem Cardinal.lift_lt_aleph1

Modified Mathlib/SetTheory/Cardinal/Basic.lean

added theorem Cardinal.aleph0_eq_lift

added theorem Cardinal.lift_eq_aleph0