union_le_add

Mathlib.Data.Multiset.UnionInter

URI: https://scilib.ai/kg/mathlib#Multiset.union_le_add

English

Distributivity of union over addition: (s ∪ t) + u = s + u ∪ (t + u).

Русский

Дистрибутивность объединения над сложением: (s ∪ t) + u = s + u ∪ (t + u).

LaTeX

$$$(s \\cup t) + u = s + u \\cup (t + u).$$$

Lean4

theorem union_le_add (s t : Multiset α) : s ∪ t ≤ s + t :=
  union_le (le_add_right ..) (le_add_left ..)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru