Theorem isGLB_le_isLUB_of_nonempty_inter

Modification history

2026-03-23 10:55
Mathlib/Order/Bounds/Basic.lean
feat(Order/ConditionallyCompleteLattice): `sInf s ≤ sSup t` for `(s ∩ t).Nonempty` (#35821)
Added isGLB_le_isLUB_of_nonempty_interView on Github →