sup_ndunion — Mathlib

English

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

Русский

Пусть α имеет полусуп и нижнюю границу. Следование объединению без дубликатов: sup(ndunion(s1,s2)) = sup(s1) ⊔ sup(s2).

LaTeX

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

Lean4

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

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