Commit 2024-10-23 09:32 5a2f1ac9

View on Github →

refactor(SetTheory/Cardinal/Aleph): aleph' → preAleph (#18099) This helps us move away from primes in theorems and definitions. Suggested by Floris van Doorn.

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Aleph.lean

deleted def Cardinal.aleph'

modified theorem Cardinal.aleph'_limit

modified theorem Cardinal.aleph'_nat

modified theorem Cardinal.aleph'_pos

modified theorem Cardinal.aleph0_le_aleph'

added theorem Cardinal.aleph0_le_preAleph

modified theorem Cardinal.aleph_eq_aleph'

added theorem Cardinal.aleph_eq_preAleph

deleted theorem Cardinal.aleph_le

added theorem Cardinal.aleph_le_aleph

deleted theorem Cardinal.aleph_lt

added theorem Cardinal.aleph_lt_aleph

modified theorem Cardinal.aleph_zero

added theorem Cardinal.lift_preAleph

added def Cardinal.preAleph

added theorem Cardinal.preAleph_isNormal

added theorem Cardinal.preAleph_le_of_isLimit

added theorem Cardinal.preAleph_le_preAleph

added theorem Cardinal.preAleph_limit

added theorem Cardinal.preAleph_lt_preAleph

added theorem Cardinal.preAleph_max

added theorem Cardinal.preAleph_nat

added theorem Cardinal.preAleph_omega0

added theorem Cardinal.preAleph_pos

added theorem Cardinal.preAleph_succ

added theorem Cardinal.preAleph_zero

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

added theorem Cardinal.isRegular_preAleph_succ

added theorem Ordinal.preAleph_cof