sum_boole_mul — Mathlib

English

For a finite set s, a function f: ι → R, and a fixed i, the sum over j in s of (indicator of i=j) times f(j) equals f(i) if i∈s and 0 otherwise.

Русский

Для конечного множества s, функции f: ι → R и фиксированного i имеем: сумма по j∈s от (индикатор{i=j})·f(j) равна f(i) при i∈s и 0 при i∉s.

LaTeX

$$$\\sum_{j\\in s} (\\mathbf{1}_{\\{i=j\\}}) f(j) = \\mathbf{1}_{\\{i\\in s\\}} f(i)$$$

Lean4

theorem sum_boole_mul (s : Finset ι) (f : ι → R) (i : ι) : ∑ j ∈ s, ite (i = j) 1 0 * f j = ite (i ∈ s) (f i) 0 := by
  simp

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