Commit 2025-07-02 18:41 ff4abc2e

View on Github →

refactor(SetTheory/Ordinal/Arithmetic): rework Ordinal.pred API (#26612) This PR does the following:

give a simpler definition of Ordinal.pred
replace ¬ ∃ a, o = succ a and ∀ a, o ≠ succ a by IsSuccPrelimit o throughout
improve theorem names

Estimated changes

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

added theorem Order.IsSuccLimit.ordinalPred_eq

added theorem Ordinal.isSuccPrelimit_lift

modified theorem Ordinal.lift_is_succ

deleted theorem Ordinal.lt_pred

added theorem Ordinal.lt_pred_iff_succ_lt

added theorem Ordinal.pred_eq_iff_isSuccPrelimit

modified theorem Ordinal.pred_eq_iff_not_succ

added theorem Ordinal.pred_eq_of_isSuccPrelimit

deleted theorem Ordinal.pred_le

added theorem Ordinal.pred_le_iff_le_succ

modified theorem Ordinal.pred_lt_iff_is_succ

added theorem Ordinal.pred_lt_iff_not_isSuccPrelimit

modified theorem Ordinal.pred_succ

added def Ordinal.pred_succ_gi

added theorem Ordinal.pred_surjective

added theorem Ordinal.self_le_succ_pred

modified theorem Ordinal.succ_lt_of_not_succ

added theorem Ordinal.succ_pred_eq_iff_not_isSuccPrelimit

modified theorem Ordinal.succ_pred_iff_is_succ

Modified Mathlib/SetTheory/Ordinal/Exponential.lean