weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero

English

A weighted sum of pairwise subtractions equals the difference of two weightedVSubOfPoint expressions.

Русский

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

LaTeX

$$$ (\\sum_{i \\in s} w_i \\,(p_1 i - p_2 i)) = s.weightedVSubOfPoint p_1 b w - s.weightedVSubOfPoint p_2 b w $$$

Lean4

/-- `weightedVSub` gives the sum of the results of subtracting any
base point, when the sum of the weights is 0. -/
theorem weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero (w : ι → k) (p : ι → P) (h : ∑ i ∈ s, w i = 0) (b : P) :
    s.weightedVSub p w = s.weightedVSubOfPoint p b w :=
  s.weightedVSubOfPoint_eq_of_sum_eq_zero w p h _ _

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