weightedVSubOfPoint_sdiff_sub — Mathlib

English

A signed-split of a weightedVSubOfPoint equals the full sum with a corresponding sign change on the second part.

Русский

Разбиение на разность по подмножествам даёт полную сумму с изменением знака второй части.

LaTeX

$$$ (s \\ s_2).weightedVSubOfPoint p b w - s_2.weightedVSubOfPoint p b (-w) = s.weightedVSubOfPoint p b w $$$

Lean4

/-- A weighted sum may be split into a subtraction of such sums over two subsets. -/
theorem weightedVSubOfPoint_sdiff_sub [DecidableEq ι] {s₂ : Finset ι} (h : s₂ ⊆ s) (w : ι → k) (p : ι → P) (b : P) :
    (s \ s₂).weightedVSubOfPoint p b w - s₂.weightedVSubOfPoint p b (-w) = s.weightedVSubOfPoint p b w := by
  rw [map_neg, sub_neg_eq_add, s.weightedVSubOfPoint_sdiff h]

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