weightedVSubOfPoint_sdiff — Mathlib

English

A weighted sum can be split into the difference of two weightedVSubOfPoint sums over two disjoint parts.

Русский

Взвешенная сумма может быть разбита на разность двух сумм weightedVSubOfPoint по двум непересекающимся частям.

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 such sums over two subsets. -/
theorem weightedVSubOfPoint_sdiff [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
  simp_rw [weightedVSubOfPoint_apply, sum_sdiff h]

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