English
Let s be a finite index set and f,g,h: s → R with the property that at a distinguished i ∈ s we have f(i) = g(i) + h(i) and for every j ∈ s with j ≠ i we have g(j) = f(j) and h(j) = f(j). Then (∏ i∈s g(i)) + (∏ i∈s h(i)) = ∏ i∈s f(i).
Русский
Пусть s - конечный индексный набор и f,g,h: s → R удовлетворяют условию: для некоторого i∈s f(i) = g(i) + h(i), а для всех j≠i в s выполняются g(j) = f(j) и h(j) = f(j). Тогда (∏ g(i)) + (∏ h(i)) = ∏ f(i).
LaTeX
$$$\\prod_{i\\in s} g(i) + \\prod_{i\\in s} h(i) = \\prod_{i\\in s} f(i)$, при условии, что $f(i) = g(i) + h(i)$ и $g(j)=f(j), h(j)=f(j)$ для всех $j\\in s$, $j\\neq i$.$$
Lean4
theorem sum_mul_boole (s : Finset ι) (f : ι → R) (i : ι) : ∑ j ∈ s, f j * ite (i = j) 1 0 = ite (i ∈ s) (f i) 0 := by
simp
