Commit 2024-12-10 02:18 e96006be

View on Github →

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

Estimated changes

Modified Mathlib/Order/SuccPred/CompleteLinearOrder.lean

modified theorem IsGLB.exists_of_not_isPredPrelimit

modified theorem IsGLB.mem_of_not_isPredPrelimit

modified theorem IsLUB.exists_of_not_isSuccPrelimit

modified theorem IsLUB.mem_of_not_isSuccPrelimit

modified theorem sInf_mem_of_not_isPredPrelimit

modified theorem sSup_mem_of_not_isSuccPrelimit