Commit 2024-09-12 06:16 381b26ac

View on Github →

feat(Order/SuccPred/Limit): IsSuccLimit (#16499) The matter of whether 0 is or not a limit element (of the ordinals/cardinals) is a highly contentious one. To bridge this gap, we redefine IsSuccLimit so as to explicitly exclude minimal elements. A previous PR had already renamed the weaker notion to IsSuccPrelimit. Future PRs will introduce the usual limit induction principles, and deprecate Cardinal.IsLimit and Ordinal.IsLimit.

Estimated changes

Modified Mathlib/Order/SuccPred/Basic.lean

added theorem Order.not_isMax_pred

added theorem Order.not_isMin_succ

Modified Mathlib/Order/SuccPred/Limit.lean

added theorem Order.IsPredLimit.lt_pred

added theorem Order.IsPredLimit.lt_pred_iff

added theorem Order.IsPredLimit.ne_top

added theorem Order.IsPredLimit.pred_ne

added def Order.IsPredLimit

added theorem Order.IsPredPrelimit.isMax_of_noMin

added theorem Order.IsPredPrelimit.isPredLimit

added theorem Order.IsPredPrelimit.isPredLimit_of_not_isMax

modified theorem Order.IsPredPrelimit.lt_pred

modified theorem Order.IsPredPrelimit.lt_pred_iff

modified theorem Order.IsPredPrelimit.pred_ne

added theorem Order.IsSuccLimit.ne_bot

added theorem Order.IsSuccLimit.succ_lt

added theorem Order.IsSuccLimit.succ_lt_iff

added theorem Order.IsSuccLimit.succ_ne

added def Order.IsSuccLimit

modified theorem Order.IsSuccPrelimit.isMin_of_noMax

added theorem Order.IsSuccPrelimit.isSuccLimit

added theorem Order.IsSuccPrelimit.isSuccLimit_of_not_isMin

added theorem Order.isPredLimit_iff

added theorem Order.isPredLimit_toDual_iff

added theorem Order.isPredPrelimit_iff_isPredLimit

added theorem Order.isPredPrelimit_iff_isPredLimit_of_not_isMax

modified theorem Order.isPredPrelimit_iff_lt_pred

modified theorem Order.isPredPrelimit_iff_of_noMin

added theorem Order.isPredPrelimit_iff_pred_ne

modified theorem Order.isPredPrelimit_of_pred_lt

added theorem Order.isSuccLimit_iff

added theorem Order.isSuccLimit_toDual_iff

added theorem Order.isSuccPrelimit_iff_isSuccLimit

added theorem Order.isSuccPrelimit_iff_isSuccLimit_of_not_isMin

modified theorem Order.isSuccPrelimit_iff_of_noMax

modified theorem Order.mem_range_pred_of_not_isPredPrelimit

modified theorem Order.mem_range_pred_or_isPredPrelimit

modified theorem Order.mem_range_succ_of_not_isSuccPrelimit

modified theorem Order.mem_range_succ_or_isSuccPrelimit

added theorem Order.not_isPredLimit

added theorem Order.not_isPredLimit_iff

added theorem Order.not_isPredLimit_of_noMin

added theorem Order.not_isPredLimit_of_not_isPredPrelimit

added theorem Order.not_isPredLimit_pred

added theorem Order.not_isPredLimit_pred_of_not_isMin

added theorem Order.not_isPredLimit_top

modified theorem Order.not_isPredPrelimit

added theorem Order.not_isPredPrelimit_iff'

modified theorem Order.not_isPredPrelimit_iff

modified theorem Order.not_isPredPrelimit_of_noMin

modified theorem Order.not_isPredPrelimit_pred

modified theorem Order.not_isPredPrelimit_pred_of_not_isMin

added theorem Order.not_isSuccLimit

added theorem Order.not_isSuccLimit_bot

added theorem Order.not_isSuccLimit_iff

added theorem Order.not_isSuccLimit_of_noMax

added theorem Order.not_isSuccLimit_succ

added theorem Order.not_isSuccLimit_succ_of_not_isMax

modified theorem Order.not_isSuccPrelimit

modified theorem Order.not_isSuccPrelimit_iff'

modified theorem Order.not_isSuccPrelimit_iff

modified theorem Order.not_isSuccPrelimit_of_noMax

modified theorem Order.not_isSuccPrelimit_succ_of_not_isMax

Modified Mathlib/SetTheory/Cardinal/Basic.lean

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean