English
The weighted sum is independent of the base point whenever the total weight is zero: for any b1,b2 ∈ P, s.weightedVSubOfPoint p b1 w = s.weightedVSubOfPoint p b2 w.
Русский
Взвешенная сумма не зависит от базовой точки, если сумма весов равна нулю: для любых b1,b2 ∈ P выполняется равенство.
LaTeX
$$If $\\sum_{i∈s} w_i = 0$, then $s.weightedVSubOfPoint p b1 w = s.weightedVSubOfPoint p b2 w$ for all base points b1,b2.$$
Lean4
/-- The weighted sum is independent of the base point when the sum of
the weights is 0. -/
theorem weightedVSubOfPoint_eq_of_sum_eq_zero (w : ι → k) (p : ι → P) (h : ∑ i ∈ s, w i = 0) (b₁ b₂ : P) :
s.weightedVSubOfPoint p b₁ w = s.weightedVSubOfPoint p b₂ w :=
by
apply eq_of_sub_eq_zero
rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply, ← sum_sub_distrib]
conv_lhs =>
congr
· skip
· ext
rw [← smul_sub, vsub_sub_vsub_cancel_left]
rw [← sum_smul, h, zero_smul]
