Theorem sInf_le_sSup_of_nonempty_inter

Modification history

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