English
Let f be defined on elements of a finite set s by f(a) for a ∈ s. Then the indicator of s with values f equals the sum over x ∈ s.attach of the singleton at x with value f(x, proof).
Русский
Пусть на конечном множестве s задана функция f; тогда индикатор s с значениями f равен сумме по x ∈ s.attach множителя с единичным вложением на x и значением f(x, доказательство).
LaTeX
$$$\operatorname{indicator} s f = \sum_{x \in s.\text{attach}} \operatorname{single} \uparrow x \big(f\, x\, x.2\big).$$$
Lean4
theorem indicator_eq_sum_attach_single [AddCommMonoid M] {s : Finset α} (f : ∀ a ∈ s, M) :
indicator s f = ∑ x ∈ s.attach, single ↑x (f x x.2) :=
by
rw [← sum_single (indicator s f), sum, sum_subset (support_indicator_subset _ _), ← sum_attach]
· refine Finset.sum_congr rfl (fun _ _ => ?_)
rw [indicator_of_mem]
· intro i _ hi
rw [notMem_support_iff.mp hi, single_zero]
