sum_prod_piFinset — Mathlib

English

If s is a finite set and g(i,·) a family of functions on each i, then the sum over f in piFinset of the product over i of g(i, f(i)) equals the product over i of the sum over j in s of g(i,j).

Русский

Если s конечно, а g(i,·) — семейство функций, то сумма по f∈piFinset произведений g(i, f(i)) равна произведению по i суммы по j∈s g(i,j).

LaTeX

$$$\\sum_{f \\in \\piFinset (\\lambda i, s)} \\prod_{i} g(i, f(i)) = \\prod_{i} \\left( \\sum_{j \\in s} g(i,j) \\right)$$$

Lean4

theorem sum_prod_piFinset [Fintype ι] (s : Finset κ) (g : ι → κ → R) :
    ∑ f ∈ piFinset fun _ : ι ↦ s, ∏ i, g i (f i) = ∏ i, ∑ j ∈ s, g i j := by rw [← prod_univ_sum]

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