English
If s and t are nonempty and every element of s is ≤ every element of t, then there exists a mediator element between the two sets; equivalently, the intersection of the upper bounds of s and the lower bounds of t is nonempty.
Русский
Если множества s и t непусты и каждый элемент s не превосходит каждого элемента t, то существует элемент между этими множествами; эквивалентно пересечение верхних границ s и нижних границ t непусто.
LaTeX
$$$\forall \alpha\, [\text{ConditionallyCompleteLattice } \alpha],\forall s,t : \text{Set }\alpha,\ s.Nonempty \to t.Nonempty \to (\forall x \in s \; \forall y \in t,\ x \le y) \to (upperBounds\ s \cap lowerBounds\ t).Nonempty$$$
Lean4
/-- If all elements of a nonempty set `s` are less than or equal to all elements
of a nonempty set `t`, then there exists an element between these sets. -/
theorem exists_between_of_forall_le (sne : s.Nonempty) (tne : t.Nonempty) (hst : ∀ x ∈ s, ∀ y ∈ t, x ≤ y) :
(upperBounds s ∩ lowerBounds t).Nonempty :=
⟨sInf t, fun x hx => le_csInf tne <| hst x hx, fun _ hy => csInf_le (sne.mono hst) hy⟩
