Theorem IsGLB.mem_of_not_isPredPrelimit

Modification history

2024-12-10 02:18

Mathlib/Order/SuccPred/CompleteLinearOrder.lean

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

Modified IsGLB.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 IsGLB.mem_of_not_isPredPrelimit View on Github →