English
Let s be a finite set of indices, let w be weights with total sum ∑ i∈s w(i) = 0, and let p be any point of the affine space. If all points considered are the same p, then the weighted virtual subtraction vanishes: weightedVSub_s (p, w) = 0.
Русский
Пусть s — конечное множество индексов, веса w с суммой ∑_{i∈s} w(i) = 0, и p — произвольная точка аффинного пространства. Если все точки равны p, то взвешенная виртуальная разность равна нулю: weightedVSub_s(p, w) = 0.
LaTeX
$$$\displaystyle s\text{.weightedVSub}( (\lambda i. p), w) = 0, \quad \text{при } \sum_{i\in s} w(i)=0.$$$
Lean4
/-- The value of `weightedVSub`, where the given points are equal and the sum of the weights
is 0. -/
@[simp]
theorem weightedVSub_apply_const (w : ι → k) (p : P) (h : ∑ i ∈ s, w i = 0) : s.weightedVSub (fun _ => p) w = 0 := by
rw [weightedVSub, weightedVSubOfPoint_apply_const, h, zero_smul]
