sup_union — Mathlib

English

For α with SemilatticeSup and OrderBot, the supremum of the union of two multisets equals the join of their supremums: (s1 ∪ s2).sup = s1.sup ⊔ s2.sup.

Русский

Пусть α имеет полусуп и нижнюю границу. Для объединения мультим множеств выполняется sup( s1 ∪ s2 ) = sup(s1) ⊔ sup(s2).

LaTeX

$$$$ (s_1 \\cup s_2).sup = s_1.sup \\sqcup s_2.sup $$$$

Lean4

@[simp]
theorem sup_union (s₁ s₂ : Multiset α) : (s₁ ∪ s₂).sup = s₁.sup ⊔ s₂.sup := by
  rw [← sup_dedup, dedup_ext.2, sup_dedup, sup_add]; simp

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