Commit 2024-10-25 18:52 970d241d

refactor: delete IsWellOrderLimitElement.lean (#15904) I understand this is quite a bold move, and I hope not to come off as confrontational. I argue that Order/IsWellOrderLimitElement.lean duplicates existing API, and that all the theorems proven within it already exist in some other form. First, note that the typeclass assumptions LinearOrder α + IsWellOrder α (· < ·) very nearly imply ConditionallyCompleteLinearOrderBot α through IsWellOrder.conditionallyCompleteLinearOrderBot. The only missing assumption is OrderBot α, which actually follows from Nonempty α through WellFoundedLT.toOrderBot. All theorems in this file assume the existence of some a : α, so that's covered. Most of the only other file importing this one assumes OrderBot α directly. ConditionallyCompleteLinearOrder α in turn implies SuccOrder α through ConditionallyCompleteLinearOrder.toSuccOrder (#15863), so assuming it yields no loss of generality. In fact, doing things this way means we can set nicer def-eqs for @succ α, such as succ o = o + 1 on ordinals. As for IsWellOrderLimitElement, we already have Order.IsSuccLimit with only trivial typeclass assumptions. To summarize, here are the correspondences between definitions and theorems in this file and other definitions and theorems in Mathlib, applicable under equivalent typeclasss assumptions:

• wellOrderSucc → Order.succ
• self_le_wellOrderSucc → Order.le_succ
• wellOrderSucc_le → Order.succ_le_of_lt
• self_lt_wellOrderSucc → Order.lt_succ_of_not_isMax
• le_of_lt_wellOrderSucc → Order.le_of_lt_succ.
• IsWellOrderLimitElement→ Order.IsSuccLimit
• IsWellOrderLimitElement.neq_bot → (already implied by IsSuccLimit)
• IsWellOrderLimitElement.bot_lt → Ne.bot_lt
• IsWellOrderLimitElement.wellOrderSucc_lt → Order.IsSuccLimit.succ_lt
• eq_bot_or_eq_succ_or_isWellOrderLimitElement → Order.isSuccLimitRecOn
• Nat.wellOrderSucc_eq → Nat.succ_eq_succ
• Nat.not_isWellOrderLimitElement → Order.IsSuccLimit.isMin_of_noMax