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]