Theorem csSup_mem_of_not_isSuccLimit

Modification history

2026-06-09 16:55
Mathlib/Order/SuccPred/CompleteLinearOrder.lean
feat(Order/SuccPred/CompleteLinearOrder): generalize `csSup_mem_of_not_isSuccLimit` (#38142) …
Modified csSup_mem_of_not_isSuccLimitView on Github →
2026-04-16 18:27
Mathlib/Order/SuccPred/CompleteLinearOrder.lean
chore: generalize cardinal supremum theorems to conditionally complete lattices (#38024)
Added csSup_mem_of_not_isSuccLimitView on Github →
2024-09-06 21:42
Mathlib/Order/SuccPred/CompleteLinearOrder.lean
refactor(Order/SuccPred/Limit): `IsSuccLimit` → `IsSuccPrelimit` (#16518) …
Deleted csSup_mem_of_not_isSuccLimitView on Github →
2023-12-19 09:58
Mathlib/Order/SuccPred/CompleteLinearOrder.lean
feat: Relation between `IsSuccLimit` and `iSup`. (#8842)
Added csSup_mem_of_not_isSuccLimitView on Github →