weightedVSub_sdiff — Mathlib

English

A weighted sum over the difference of two finite sets equals the sum over the whole set: (s \ s2).weightedVSub p w + s2.weightedVSub p w = s.weightedVSub p w, provided DecidableEq on indices.

Русский

Взвешенная сумма по разности конечных множеств равна сумме по всему множеству.

LaTeX

$$$ (s \\ s_2).weightedVSub p w + s_2.weightedVSub p w = s.weightedVSub p w $$$

Lean4

/-- A weighted sum may be split into such sums over two subsets. -/
theorem weightedVSub_sdiff [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 h _ _ _

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