add_inter_distrib

Mathlib.Data.Multiset.UnionInter

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

← MathLib Explorer

English

Let s, t, u be multisets. Then s + t ∩ u = (s + t) ∩ (s + u).

Русский

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

LaTeX

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

Lean4

theorem add_inter_distrib (s t u : Multiset α) : s + t ∩ u = (s + t) ∩ (s + u) := by
  rw [Multiset.add_comm, inter_add_distrib, s.add_comm, s.add_comm]

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

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

Разделы

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

Аффилиация

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