sum_ite_self_eq' — Mathlib

English

A restatement of sum_ite_self_eq' with the test reversed: (f.sum (λ x v, ite (x = a) v 0)) equals f(a).

Русский

Переформулировка sum_ite_self_eq' с обращенным тестом: (f.sum (λ x v, ite (x = a) v 0)) равно f(a).

LaTeX

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

Lean4

/-- A restatement of `sum_ite_self_eq` with the equality test reversed. -/
theorem sum_ite_self_eq' [DecidableEq α] {N : Type*} [AddCommMonoid N] (f : α →₀ N) (a : α) :
    (f.sum fun x v => ite (x = a) v 0) = f a := by simp

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