Theorem IsGLB.mem_of_not_isPredPrelimit
Modification history
2025-02-17 21:24
Mathlib/Order/SuccPred/CompleteLinearOrder.lean
feat: generalize `IsLUB.mem_of_not_isSuccPrelimit` to `LinearOrder` (#20502)
Modified IsGLB.mem_of_not_isPredPrelimitView on Github →