English
Folding over a disjoint sum distributes: fold op (op b1 b2) f (s.disjSum t) = op (fold op b1 (f ∘ inl) s) (fold op b2 (f ∘ inr) t).
Русский
Сведение по дизьитной сумме распределяется: fold op (op b1 b2) f (s.disjSum t) = op (fold op b1 (f ∘ inl) s) (fold op b2 (f ∘ inr) t).
LaTeX
$$$\\mathrm{fold}\, op\\ (op\\ b_1\\ b_2)\\ f\\ (s.disjSum t) = op\\left( s.fold\\ op\\ b_1\\ (f \\langle \\cdot \\rangle \\mathrm{inl}) s \\right)\\left( t.fold\\ op\\ b_2\\ (f \\langle \\cdot \\rangle \\mathrm{inr}) t \\right)$$$
Lean4
theorem fold_disjSum (s : Finset α) (t : Finset β) (f : α ⊕ β → γ) (b₁ b₂ : γ) (op : γ → γ → γ) [Std.Commutative op]
[Std.Associative op] :
(s.disjSum t).fold op (op b₁ b₂) f = op (s.fold op b₁ (f <| .inl ·)) (t.fold op b₂ (f <| .inr ·)) := by
simp_rw [fold, disjSum, Multiset.map_disjSum, fold_add]
