weightedVSub_vadd — Mathlib

English

Adding a vector v to the base point inside the input for weightedVSub does not change the result, provided the sum of weights is zero.

Русский

При добавлении вектора v к базовой точке внутри аргументов weightedVSub результат не меняется, если сумма весов равна нулю.

LaTeX

$$$\displaystyle s.weightedVSub (v \,+\_v p) \ w = s.weightedVSub p w$$$

Lean4

theorem weightedVSub_vadd {s : Finset ι} {w : ι → k} (h : ∑ i ∈ s, w i = 0) (p : ι → P) (v : V) :
    s.weightedVSub (v +ᵥ p) w = s.weightedVSub p w := by
  rw [weightedVSub, weightedVSubOfPoint_vadd, weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero _ _ _ h]

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