Commit 2025-07-11 17:39 d6f4a825

View on Github →

refactor(SetTheory/Ordinal/Arithmetic): Ordinal.IsLimit → Order.IsSuccLimit (#26643) This is part of a series of ordinal refactors which aim to replace definitions specific to Ordinal with more general concepts. See #17033 for more info.

Estimated changes

Modified Mathlib/MeasureTheory/MeasurableSpace/Card.lean

Modified Mathlib/Order/SuccPred/Limit.lean

Modified Mathlib/SetTheory/Cardinal/Aleph.lean

modified theorem Cardinal.aleph_limit

modified theorem Cardinal.beth_limit

deleted theorem Cardinal.isLimit_omega

added theorem Cardinal.isSuccLimit_omega

deleted theorem Cardinal.preAleph_le_of_isLimit

added theorem Cardinal.preAleph_le_of_isSuccPrelimit

modified theorem Cardinal.preAleph_limit

Modified Mathlib/SetTheory/Cardinal/Arithmetic.lean

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

modified theorem Ordinal.IsNormal.cof_eq

modified theorem Ordinal.aleph0_le_cof

modified theorem Ordinal.cof_eq'

modified theorem Ordinal.cof_omega

Modified Mathlib/SetTheory/Cardinal/Ordinal.lean

Modified Mathlib/SetTheory/Cardinal/Regular.lean

modified theorem Cardinal.isRegular_cof

Modified Mathlib/SetTheory/Game/Birthday.lean

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

deleted theorem Cardinal.isLimit_ord

added theorem Cardinal.isSuccLimit_ord

deleted theorem Ordinal.IsLimit.iSup_Iio

deleted theorem Ordinal.IsLimit.isSuccPrelimit

deleted theorem Ordinal.IsLimit.nat_lt

deleted theorem Ordinal.IsLimit.one_lt

deleted theorem Ordinal.IsLimit.sSup_Iio

deleted theorem Ordinal.IsLimit.succ_lt

deleted theorem Ordinal.IsNormal.isLimit

added theorem Ordinal.IsNormal.isSuccLimit

modified theorem Ordinal.IsNormal.limit_lt

added theorem Ordinal.add_le_iff_of_isSuccLimit

deleted theorem Ordinal.add_le_of_limit

deleted theorem Ordinal.add_mul_limit

added theorem Ordinal.add_mul_of_isSuccLimit

modified def Ordinal.boundedLimitRecOn

modified theorem Ordinal.boundedLimitRec_limit

modified theorem Ordinal.boundedLimitRec_succ

modified theorem Ordinal.boundedLimitRec_zero

modified theorem Ordinal.bounded_singleton

deleted theorem Ordinal.isLimit_add

deleted theorem Ordinal.isLimit_add_iff

deleted theorem Ordinal.isLimit_iff

deleted theorem Ordinal.isLimit_iff_omega0_dvd

deleted theorem Ordinal.isLimit_mul

deleted theorem Ordinal.isLimit_mul_left

deleted theorem Ordinal.isLimit_omega0

deleted theorem Ordinal.isLimit_sub

added theorem Ordinal.isSuccLimit_add

added theorem Ordinal.isSuccLimit_add_iff

added theorem Ordinal.isSuccLimit_iff

added theorem Ordinal.isSuccLimit_iff_omega0_dvd

added theorem Ordinal.isSuccLimit_lift

added theorem Ordinal.isSuccLimit_mul

added theorem Ordinal.isSuccLimit_mul_left

added theorem Ordinal.isSuccLimit_omega0

added theorem Ordinal.isSuccLimit_sub

modified theorem Ordinal.isSuccPrelimit_lift

deleted theorem Ordinal.le_succ_of_isLimit

deleted theorem Ordinal.lift_isLimit

deleted theorem Ordinal.limit_le

deleted theorem Ordinal.lt_limit

added theorem Ordinal.lt_mul_iff_of_isSuccLimit

deleted theorem Ordinal.lt_mul_of_limit

added theorem Ordinal.mul_le_iff_of_isSuccLimit

deleted theorem Ordinal.mul_le_of_limit

added theorem Ordinal.natCast_lt_of_isSuccLimit

deleted theorem Ordinal.nat_lt_limit

added theorem Ordinal.not_isSuccLimit_zero

deleted theorem Ordinal.not_succ_isLimit

deleted theorem Ordinal.not_zero_isLimit

deleted theorem Ordinal.omega0_le_of_isLimit

added theorem Ordinal.omega0_le_of_isSuccLimit

added theorem Ordinal.one_lt_of_isSuccLimit

deleted theorem Ordinal.succ_lt_of_isLimit

added theorem Ordinal.zero_or_succ_or_isSuccLimit

Modified Mathlib/SetTheory/Ordinal/Enum.lean

Modified Mathlib/SetTheory/Ordinal/Exponential.lean

deleted theorem Ordinal.isLimit_opow

deleted theorem Ordinal.isLimit_opow_left

added theorem Ordinal.isSuccLimit_opow

added theorem Ordinal.isSuccLimit_opow_left

added theorem Ordinal.lt_opow_of_isSuccLimit

deleted theorem Ordinal.lt_opow_of_limit

added theorem Ordinal.opow_le_of_isSuccLimit

deleted theorem Ordinal.opow_le_of_limit

modified theorem Ordinal.opow_limit

Modified Mathlib/SetTheory/Ordinal/Family.lean

deleted theorem Ordinal.IsNormal.apply_of_isLimit

added theorem Ordinal.IsNormal.apply_of_isSuccLimit

modified theorem Ordinal.bsup_eq_blsub_of_lt_succ_limit

modified theorem Ordinal.lt_add_of_limit

Modified Mathlib/SetTheory/Ordinal/FixedPoint.lean

modified theorem Ordinal.deriv_limit

Modified Mathlib/SetTheory/Ordinal/NaturalOps.lean

Modified Mathlib/SetTheory/Ordinal/Notation.lean

Modified Mathlib/SetTheory/Ordinal/Principal.lean

deleted theorem Ordinal.isLimit_of_principal_add

deleted theorem Ordinal.isLimit_of_principal_mul

added theorem Ordinal.isSuccLimit_of_principal_add

added theorem Ordinal.isSuccLimit_of_principal_mul

Modified Mathlib/SetTheory/Ordinal/Topology.lean

deleted theorem Ordinal.IsAcc.isLimit

added theorem Ordinal.IsAcc.isSuccLimit

deleted theorem Ordinal.isLimit_of_mem_frontier

modified theorem Ordinal.isOpen_iff

modified theorem Ordinal.isOpen_singleton_iff

added theorem Ordinal.isSuccLimit_of_mem_frontier

modified theorem Ordinal.nhds_eq_pure

Modified Mathlib/SetTheory/Ordinal/Veblen.lean

Modified Mathlib/Topology/Category/Profinite/Nobeling/Induction.lean

modified theorem Profinite.NobelingProof.GoodProducts.Plimit

Modified Mathlib/Topology/Category/Profinite/Nobeling/ZeroLimit.lean