sSup_union — Mathlib

English

The supremum of the union of two sets equals the join of their suprema: sSup(s ∪ t) = sSup(s) ⊔ sSup(t).

Русский

Супремум объединения двух множеств равен присоединению их супремумов: sSup(s ∪ t) = sSup(s) ⊔ sSup(t).

LaTeX

$$$$ \operatorname{sSup}(s \cup t) = \operatorname{sSup}(s) \sqcup \operatorname{sSup}(t) $$$$

Lean4

theorem sSup_union {s t : Set α} : sSup (s ∪ t) = sSup s ⊔ sSup t :=
  ((isLUB_sSup s).union (isLUB_sSup t)).sSup_eq

Похожие утверждения