English
Let op be a commutative and associative binary operation on α, and s1,s2 be multisets of α. For b1,b2∈α, the fold over the union of s1 and s2 with initial b1, times the fold over the intersection with initial b2, equals the product of the folds over s1 and s2 with their respective initial values:\n((s1 ∪ s2).fold op b1) * ((s1 ∩ s2).fold op b2) = (s1.fold op b1) * (s2.fold op b2).
Русский
Пусть op — коммутативная и ассоциативная бинарная операция на α, s1,s2 — мультисеты. Тогда произведение свёрток по объединению с начальным b1 и по пересечению с начальным b2 равно произведению свёрток по каждому из множества отдельно:
LaTeX
$$$\\big(\\operatorname{fold}_{\\otimes} b_1 (s_1 \\cup s_2)\\big) \\cdot \\big(\\operatorname{fold}_{\\otimes} b_2 (s_1 \\cap s_2)\\big) = \\operatorname{fold}_{\\otimes} b_1 s_1 \\cdot \\operatorname{fold}_{\\otimes} b_2 s_2$$$
Lean4
theorem fold_union_inter [DecidableEq α] (s₁ s₂ : Multiset α) (b₁ b₂ : α) :
((s₁ ∪ s₂).fold op b₁ * (s₁ ∩ s₂).fold op b₂) = s₁.fold op b₁ * s₂.fold op b₂ := by
rw [← fold_add op, union_add_inter, fold_add op]
