weightedVSub_sdiff_sub — Mathlib

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 _ _ _

Похожие утверждения