English
The supremum of an intersection is bounded above by the minimum of the suprema: sSup(s ∩ t) ≤ sSup s ⊓ sSup t, assuming s,t bounded above and their intersection nonempty.
Русский
Наибольшая граница пересечения ограничена снизу минимумом из верхних пределов: sSup(s ∩ t) ≤ sSup s ⊓ sSup t, при условии ограниченности сверху и непустоты пересечения.
LaTeX
$$$\forall s,t:\\text{Set }\alpha,\ BddAbove\ s \\to BddAbove\ t \\to (s \cap t).Nonempty \\to sSup(s\cap t) \le sSup s \sqcap sSup t$$$
Lean4
/-- The supremum of an intersection of two sets is bounded by the minimum of the suprema of each
set, if all sets are bounded above and nonempty. -/
theorem csSup_inter_le (hs : BddAbove s) (ht : BddAbove t) (hst : (s ∩ t).Nonempty) : sSup (s ∩ t) ≤ sSup s ⊓ sSup t :=
(csSup_le hst) fun _ hx => le_inf (le_csSup hs hx.1) (le_csSup ht hx.2)
