Theorem exists_eq_ciSup_of_not_isSuccPrelimit'

Modification history

2026-06-09 16:55
Mathlib/Order/SuccPred/CompleteLinearOrder.lean
feat(Order/SuccPred/CompleteLinearOrder): generalize `csSup_mem_of_not_isSuccLimit` (#38142) …
Deleted exists_eq_ciSup_of_not_isSuccPrelimit'View on Github →
2026-04-16 18:27
Mathlib/Order/SuccPred/CompleteLinearOrder.lean
chore: generalize cardinal supremum theorems to conditionally complete lattices (#38024)
Modified exists_eq_ciSup_of_not_isSuccPrelimit'View on Github →
2024-09-06 21:42
Mathlib/Order/SuccPred/CompleteLinearOrder.lean
refactor(Order/SuccPred/Limit): `IsSuccLimit` → `IsSuccPrelimit` (#16518) …
Added exists_eq_ciSup_of_not_isSuccPrelimit'View on Github →