English
For f: κ → α, s a finite set of κ, and i ∈ ι, the sum over the piFinset of s of f(g i) equals |s|^{card ι − 1} times the sum over s of f.
Русский
Для f: κ → α, конечного множества s ⊆ κ и i ∈ ι: сумма по g в piFinset(fun _ => s) f(g i) равна |s|^{card ι − 1} умножить на сумму по b∈ s f(b).
LaTeX
$$$$ \\sum g \\in \\piFinset (\\lambda _ : ι, s), f(g(i)) = |s|^{\\left|ι\\right| - 1} \\cdot \\sum_{b \in s} f(b). $$$$
Lean4
theorem sum_piFinset_apply (f : κ → α) (s : Finset κ) (i : ι) :
∑ g ∈ piFinset fun _ : ι ↦ s, f (g i) = #s ^ (card ι - 1) • ∑ b ∈ s, f b := by
classical
rw [Finset.sum_comp]
simp only [eval_image_piFinset_const, card_filter_piFinset_const s, ite_smul, zero_smul, smul_sum, Finset.sum_ite_mem,
inter_self]
