cons_inter_distrib

Mathlib.Data.Multiset.UnionInter

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

English

Let a be an element and s, t multisets. Then a :: (s ∩ t) = (a :: s) ∩ (a :: t).

Русский

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

LaTeX

$$$ \\text{cons}(a, s \\cap t) = \\text{cons}(a, s) \\cap \\text{cons}(a, t) $$$

Lean4

theorem cons_inter_distrib (a : α) (s t : Multiset α) : a ::ₘ s ∩ t = (a ::ₘ s) ∩ (a ::ₘ t) := by simp

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

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

Разделы

Аффилиация

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