indicator_eq_sum_single — Mathlib

English

For any finite set s, and any function f on s, the indicator function indicator s (fun x _ ↦ f x) equals the sum over x ∈ s of the singleton at x with value f x.

Русский

Для конечного множества s и функции f на s индикатор indicator s (fun x _ ↦ f x) равен сумме по x ∈ s от одинокого элемента x с значением f x.

LaTeX

$$$\operatorname{indicator} s (\lambda x \_ , f x) = \sum_{x \in s} \operatorname{single} x (f x).$$$

Lean4

theorem indicator_eq_sum_single [AddCommMonoid M] (s : Finset α) (f : α → M) :
    indicator s (fun x _ ↦ f x) = ∑ x ∈ s, single x (f x) :=
  (indicator_eq_sum_attach_single _).trans <| sum_attach _ fun x ↦ single x (f x)

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