English
The supremum of the union equals the join of the suprema: sSup(s ∪ t) = sSup s ⊔ sSup t, provided s and t are nonempty and bounded above.
Русский
Наибольшая верхняя граница объединения равна объединению верхних границ: sSup(s ∪ t) = sSup s ⊔ sSup t, если s и t непусты и ограничены сверху.
LaTeX
$$$\forall s,t:\\text{Set }\alpha,\ BddAbove\ s → s.Nonempty \\to BddAbove\ t → t.Nonempty \\to sSup(s\cup t) = sSup s \sqcup sSup t$$$
Lean4
/-- The `sSup` of a union of two sets is the max of the suprema of each subset, under the
assumptions that all sets are bounded above and nonempty. -/
theorem csSup_union (hs : BddAbove s) (sne : s.Nonempty) (ht : BddAbove t) (tne : t.Nonempty) :
sSup (s ∪ t) = sSup s ⊔ sSup t :=
((isLUB_csSup sne hs).union (isLUB_csSup tne ht)).csSup_eq sne.inl
