English
A refined version: (s \ s2).weightedVSub p w − s2.weightedVSub p (−w) = s.weightedVSub p w, for DecidableEq ι and subset s2 ⊆ s.
Русский
Уточненная версия: разность weightedVSub по разности и weightedVSub по части равна WeightedVSub по всему множеству.
LaTeX
$$$ (s \ s_2).weightedVSub p w - s_2.weightedVSub p (-w) = s.weightedVSub p w $$$
Lean4
/-- A weighted sum may be split into a subtraction of such sums over two subsets. -/
theorem weightedVSub_sdiff_sub [DecidableEq ι] {s₂ : Finset ι} (h : s₂ ⊆ s) (w : ι → k) (p : ι → P) :
(s \ s₂).weightedVSub p w - s₂.weightedVSub p (-w) = s.weightedVSub p w :=
s.weightedVSubOfPoint_sdiff_sub h _ _ _