English
Let f be a finitely supported function f: α → M and let a ∈ α. For any b: α → M → N, the product over α of the values ite(a = x) (b x (f x)) 1 equals b(a, f(a)) if a is in the support of f, and equals 1 otherwise.
Русский
Пусть f: α →₀ M — конечно-поддерживаемая функция и возьмем a ∈ α. Для любой b: α → M → N справедливо, что произведение по x ∈ α⋯ ite(a = x) (b x (f x)) 1 равно b(a, f(a)) при условии, что a принадлежит поддержке f, и равно 1 в противном случае.
LaTeX
$$$$ (f \\mathrm{.prod} \\; b) = \\begin{cases} b(a, f(a)) & \\text{если } a \\in \\mathrm{supp}(f), \\\\ 1 & \\text{иначе}. \\end{cases} $$$$
Lean4
@[to_additive (attr := simp)]
theorem prod_ite_eq [DecidableEq α] (f : α →₀ M) (a : α) (b : α → M → N) :
(f.prod fun x v => ite (a = x) (b x v) 1) = ite (a ∈ f.support) (b a (f a)) 1 :=
by
dsimp [Finsupp.prod]
rw [f.support.prod_ite_eq]
