sup_add — Mathlib

English

For multisets s1 and s2, the supremum of their sum equals the supremum of their individual suprema: sup(s1 + s2) = sup(s1) ⊔ sup(s2).

Русский

Супремум суммы мультсетів равен объединению их супремумов: sup(s1+s2) = sup(s1) ⊔ sup(s2).

LaTeX

$$$\\operatorname{sup}(s_1 + s_2) = \\operatorname{sup}(s_1) \\;\\sqcup\\; \\operatorname{sup}(s_2)$$$

Lean4

@[simp]
theorem sup_add (s₁ s₂ : Multiset α) : (s₁ + s₂).sup = s₁.sup ⊔ s₂.sup :=
  Eq.trans (by simp [sup]) (fold_add _ _ _ _ _)

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