English
Replacing weights by an indicator of a subset, while expanding the index set, does not change the result of WeightedVSub when the subset relation holds.
Русский
Замена весов на индикатор подмножества и расширение индекса не меняют WeightedVSub при условии включения.
LaTeX
$$$s_1\subseteq s_2 \Rightarrow s_1.weightedVSub(p,w)=s_2.weightedVSub(p,\mathrm{indicator}(\uparrow s_1)\, w)$$$
Lean4
/-- The weighted sum is unaffected by changing the weights to the
corresponding indicator function and adding points to the set. -/
theorem weightedVSub_indicator_subset (w : ι → k) (p : ι → P) {s₁ s₂ : Finset ι} (h : s₁ ⊆ s₂) :
s₁.weightedVSub p w = s₂.weightedVSub p (Set.indicator (↑s₁) w) :=
weightedVSubOfPoint_indicator_subset _ _ _ h