add_union_distrib

Mathlib.Data.Multiset.UnionInter

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

← MathLib Explorer

English

Let s, t, u be multisets over a type α. Then s + (t ∪ u) = (s + t) ∪ (s + u).

Русский

Пусть s, t, u — мультимножества над типом α. Тогда s + (t ∪ u) = (s + t) ∪ (s + u).

LaTeX

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

Lean4

theorem add_union_distrib (s t u : Multiset α) : s + (t ∪ u) = s + t ∪ (s + u) := by
  rw [Multiset.add_comm, union_add_distrib, s.add_comm, s.add_comm]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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