Commit 2024-12-05 05:55 6a9d0fe9

View on Github →

refactor(SetTheory/Ordinal/Arithmetic): redefine IsLimit to IsSuccLimit (#19054) This is a temporary stepping stone before outright deprecating IsLimit.

Estimated changes

Modified Mathlib/Order/SuccPred/Limit.lean

added theorem Order.IsSuccLimit.bot_lt

added theorem Order.isMin_or_mem_range_succ_or_isSuccLimit

Modified Mathlib/SetTheory/Cardinal/Arithmetic.lean

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

added theorem Ordinal.IsLimit.ne_zero

modified theorem Ordinal.IsNormal.isLimit

added theorem Ordinal.isLimit_iff

modified theorem Ordinal.isLimit_omega0

modified theorem Ordinal.isLimit_sub

modified theorem Ordinal.limitRecOn_zero

modified theorem Ordinal.not_succ_isLimit

modified theorem Ordinal.not_zero_isLimit

Modified Mathlib/SetTheory/Ordinal/Notation.lean

Modified Mathlib/SetTheory/Ordinal/Principal.lean

modified theorem Ordinal.isLimit_of_principal_add

Modified Mathlib/SetTheory/Ordinal/Topology.lean

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