sum_ite_self_eq — Mathlib

English

Let f be a finitely supported function f: α → N and a ∈ α. Then summing over x of the term that is v when x = a and 0 otherwise yields f(a): ∑x (ite(a = x) f(x)) = f(a).

Русский

Пусть f: α →₀ N; тогда сумма по x от тэга, равного f(x) при x = a и нуля при остальных, равна f(a).

LaTeX

$$$$ (f \\mathrm{sum} (\\\\lambda x v. \\text{ite}(a = x) v 0)) = f a $$$$

Lean4

theorem sum_ite_self_eq [DecidableEq α] {N : Type*} [AddCommMonoid N] (f : α →₀ N) (a : α) :
    (f.sum fun x v => ite (a = x) v 0) = f a := by simp_all

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