sum_smul_vsub_eq_weightedVSub_sub

English

A weighted sum of pairwise vector differences equals the difference of two weightedVSub expressions.

Русский

Взвешенная сумма разниц векторов равна разности двух выражений weightedVSub.

LaTeX

$$$\displaystyle \sum_{i\in s} w_i\,\big(p_1(i)-\!_v\,p_2(i)\big) = s.weightedVSub(p_1,w) - s.weightedVSub(p_2,w)$$$

Lean4

/-- A weighted sum of pairwise subtractions, expressed as a subtraction of two `weightedVSub`
expressions. -/
theorem sum_smul_vsub_eq_weightedVSub_sub (w : ι → k) (p₁ p₂ : ι → P) :
    (∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i)) = s.weightedVSub p₁ w - s.weightedVSub p₂ w :=
  s.sum_smul_vsub_eq_weightedVSubOfPoint_sub _ _ _ _

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