English
For Finsets s1, s2 and a commutative associative operation, folding over the union and intersection yields a relation between the two folds.
Русский
Для Finset s1, s2 и операций свёртки выполняется связь между свёртками по объединению и пересечению.
LaTeX
$$$((s_1 \\cup s_2).fold op b_1 f * (s_1 \\cap s_2).fold op b_2 f) = s_1.fold op b_2 f * s_2.fold op b_1 f$$$
Lean4
theorem fold_union_inter [DecidableEq α] {s₁ s₂ : Finset α} {b₁ b₂ : β} :
((s₁ ∪ s₂).fold op b₁ f * (s₁ ∩ s₂).fold op b₂ f) = s₁.fold op b₂ f * s₂.fold op b₁ f :=
by
unfold fold
rw [← fold_add op, ← Multiset.map_add, union_val, inter_val, union_add_inter, Multiset.map_add, hc.comm, fold_add]
