Theorem eq_bot_or_eq_succ_or_isWellOrderLimitElement

Modification history

2024-10-25 18:52
Mathlib/Order/IsWellOrderLimitElement.lean
refactor: delete IsWellOrderLimitElement.lean (#15904) …
Deleted eq_bot_or_eq_succ_or_isWellOrderLimitElementView on Github →
2024-04-16 22:37
Mathlib/Order/IsWellOrderLimitElement.lean
feat(Order): limit elements in well-ordered types (#11584) …
Added eq_bot_or_eq_succ_or_isWellOrderLimitElementView on Github →