English
Changing the weights to the indicator function of a subset does not affect the weightedVSubOfPoint when restricted to that subset.
Русский
Изменение весов на индикатор подмножества не влияет на weightedVSubOfPoint при ограничении к этому подмножеству.
LaTeX
$$$ w \\mapsto s.weightedVSubOfPoint p b w = s.weightedVSubOfPoint p b (\\mathbf{1}_{s} \\cdot w) $$$
Lean4
/-- The weighted sum is unaffected by changing the weights to the
corresponding indicator function and adding points to the set. -/
theorem weightedVSubOfPoint_indicator_subset (w : ι → k) (p : ι → P) (b : P) {s₁ s₂ : Finset ι} (h : s₁ ⊆ s₂) :
s₁.weightedVSubOfPoint p b w = s₂.weightedVSubOfPoint p b (Set.indicator (↑s₁) w) :=
by
rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply]
exact Eq.symm <| sum_indicator_subset_of_eq_zero w (fun i wi => wi • (p i -ᵥ b : V)) h fun i => zero_smul k _
