English
If i belongs to t, then the center of mass of the indicator weights (1 at i and 0 elsewhere) picks out the i-th element: t.centerMass of the indicator weights equals z_i.
Русский
Если i принадлежит t, то центр массы для весов, равных 1 в позиции i и 0 в остальных, даёт z_i.
LaTeX
$$t.centerMass\, (i \mapsto \mathbf{1}_{i})\, z = z_i$$
Lean4
theorem centerMass_ite_eq [DecidableEq ι] (hi : i ∈ t) : t.centerMass (fun j => if i = j then (1 : R) else 0) z = z i :=
by
rw [Finset.centerMass_eq_of_sum_1]
· trans ∑ j ∈ t, if i = j then z i else 0
· congr with i
split_ifs with h
exacts [h ▸ one_smul _ _, zero_smul _ _]
· rw [sum_ite_eq, if_pos hi]
· rw [sum_ite_eq, if_pos hi]