Theorem sInf_mem_of_not_isPredPrelimit

Modification history

2024-12-10 02:18

Mathlib/Order/SuccPred/CompleteLinearOrder.lean

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

Modified sInf_mem_of_not_isPredPrelimit View on Github →

2024-09-06 21:42

Mathlib/Order/SuccPred/CompleteLinearOrder.lean

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

Added sInf_mem_of_not_isPredPrelimit View on Github →