fold_disjUnion — Mathlib

English

For disjoint Finsets s1 and s2, folding over their disjoint union equals the product of folds over each set with corresponding seeds.

Русский

Для несмежных множеств s1, s2 свёртка по их дизъюнкции равна произведению свёрток по каждому множеству с соответствующими начальными значениями.

LaTeX

$$$(s_1 \\disjUnion s_2\\ h).fold op (b_1 * b_2) f = s_1.fold op b_1 f * s_2.fold op b_2 f$$$

Lean4

theorem fold_disjUnion {s₁ s₂ : Finset α} {b₁ b₂ : β} (h) :
    (s₁.disjUnion s₂ h).fold op (b₁ * b₂) f = s₁.fold op b₁ f * s₂.fold op b₂ f :=
  (congr_arg _ <| Multiset.map_add _ _ _).trans (Multiset.fold_add _ _ _ _ _)

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