evalEval_finset_sum — Mathlib

English

For a finite index set, evaluation commutes with finite sums: evaluating the sum ∑ i∈s f(i) yields the sum of evaluations.

Русский

Для конечного индекса s вычисление суммы ∑ i∈s f(i) коммутирует с вычислением: суммарное значение равно сумме значений.

LaTeX

$$$ (\\sum\\ i\\in s, f\\ i).evalEval\\ x\\ y = \\sum\\ i\\in s, (f\\ i).evalEval\\ x\\ y $$$

Lean4

theorem evalEval_finset_sum {ι : Type*} (s : Finset ι) (x y : R) (f : ι → R[X][Y]) :
    (∑ i ∈ s, f i).evalEval x y = ∑ i ∈ s, (f i).evalEval x y := by simp only [evalEval, eval_finset_sum]

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