Theorem csInf_le_csSup_of_nonempty_inter

Modification history

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