Theorem sSup_mem_of_not_isSuccPrelimit

Modification history

2024-12-10 02:18

Mathlib/Order/SuccPred/CompleteLinearOrder.lean

chore(Order/SuccPred/CompleteLinearOrder): spacing fixes (#19799)

Modified sSup_mem_of_not_isSuccPrelimit View on Github →

2024-09-06 21:42

Mathlib/Order/SuccPred/CompleteLinearOrder.lean

refactor(Order/SuccPred/Limit): `IsSuccLimit` → `IsSuccPrelimit` (#16518) …

Added sSup_mem_of_not_isSuccPrelimit View on Github →