Commit 2026-04-05 15:16 58df4fc8

View on Github →

feat: many simp lemmas about aleph/beth/omega functions and lift (#37363)

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Aleph.lean

added theorem Cardinal.aleph_natCast_eq_lift

added theorem Cardinal.aleph_natCast_le_lift

added theorem Cardinal.aleph_natCast_lt_lift

added theorem Cardinal.aleph_ofNat_eq_lift

added theorem Cardinal.aleph_ofNat_le_lift

added theorem Cardinal.aleph_ofNat_lt_lift

modified theorem Cardinal.aleph_one_eq_lift

modified theorem Cardinal.aleph_one_le_lift

modified theorem Cardinal.aleph_one_lt_lift

added theorem Cardinal.beth_natCast_eq_lift

added theorem Cardinal.beth_natCast_le_lift

added theorem Cardinal.beth_natCast_lt_lift

added theorem Cardinal.beth_ofNat_eq_lift

added theorem Cardinal.beth_ofNat_le_lift

added theorem Cardinal.beth_ofNat_lt_lift

added theorem Cardinal.lift_eq_aleph_natCast

added theorem Cardinal.lift_eq_aleph_ofNat

modified theorem Cardinal.lift_eq_aleph_one

added theorem Cardinal.lift_eq_beth_natCast

added theorem Cardinal.lift_eq_beth_ofNat

added theorem Cardinal.lift_le_aleph_natCast

added theorem Cardinal.lift_le_aleph_ofNat

modified theorem Cardinal.lift_le_aleph_one

added theorem Cardinal.lift_le_beth_natCast

added theorem Cardinal.lift_le_beth_ofNat

added theorem Cardinal.lift_lt_aleph_natCast

added theorem Cardinal.lift_lt_aleph_ofNat

modified theorem Cardinal.lift_lt_aleph_one

added theorem Cardinal.lift_lt_beth_natCast

added theorem Cardinal.lift_lt_beth_ofNat

added theorem Ordinal.lift_eq_omega_natCast

added theorem Ordinal.lift_eq_omega_ofNat

added theorem Ordinal.lift_eq_omega_one

added theorem Ordinal.lift_le_omega_natCast

added theorem Ordinal.lift_le_omega_ofNat

added theorem Ordinal.lift_le_omega_one

added theorem Ordinal.lift_lt_omega_natCast

added theorem Ordinal.lift_lt_omega_ofNat

added theorem Ordinal.lift_lt_omega_one

added theorem Ordinal.omega_natCast_eq_lift

added theorem Ordinal.omega_natCast_le_lift

added theorem Ordinal.omega_natCast_lt_lift

added theorem Ordinal.omega_ofNat_eq_lift

added theorem Ordinal.omega_ofNat_le_lift

added theorem Ordinal.omega_ofNat_lt_lift

added theorem Ordinal.omega_one_eq_lift

added theorem Ordinal.omega_one_le_lift

added theorem Ordinal.omega_one_lt_lift