Commit 2025-12-22 18:39 2a7a4af5

View on Github →

refactor: standardize spelling of ℵ₁ as aleph_one (#33198) See Zulip.

Estimated changes

Modified Mathlib/MeasureTheory/MeasurableSpace/Card.lean

deleted theorem MeasurableSpace.generateMeasurableRec_of_omega1_le

added theorem MeasurableSpace.generateMeasurableRec_of_omega_one_le

deleted theorem MeasurableSpace.generateMeasurableRec_omega1

added theorem MeasurableSpace.generateMeasurableRec_omega_one

Modified Mathlib/SetTheory/Cardinal/Aleph.lean

deleted theorem Cardinal.aleph1_eq_lift

deleted theorem Cardinal.aleph1_le_lift

deleted theorem Cardinal.aleph1_lt_lift

added theorem Cardinal.aleph_one_eq_lift

added theorem Cardinal.aleph_one_le_lift

added theorem Cardinal.aleph_one_lt_lift

deleted theorem Cardinal.lift_eq_aleph1

added theorem Cardinal.lift_eq_aleph_one

deleted theorem Cardinal.lift_le_aleph1

added theorem Cardinal.lift_le_aleph_one

deleted theorem Cardinal.lift_lt_aleph1

added theorem Cardinal.lift_lt_aleph_one

deleted theorem Ordinal.omega0_lt_omega1

added theorem Ordinal.omega0_lt_omega_one

Modified Mathlib/SetTheory/Cardinal/Defs.lean

Modified Mathlib/SetTheory/Cardinal/Regular.lean

deleted theorem Ordinal.iSup_sequence_lt_omega1

added theorem Ordinal.iSup_sequence_lt_omega_one

Modified Mathlib/SetTheory/Ordinal/Basic.lean