English
If a weight w_i equals −1 and all other weights in the set are zero, then the affine combination over the remaining indices equals the omitted point p_i.
Русский
Если один вес равен −1 и все другие веса нули, то аффинная комбинация по оставшимся точкам равна исключённой точке.
LaTeX
$$$$ \text{If } w_i=-1\text{ and } w_j=0\ (j\neq i),\; {x \in s| x\neq i}.affineCombination k(p,w)= p_i. $$$$
Lean4
/-- If a weighted sum is zero and one of the weights is `-1`, the corresponding point is
the affine combination of the other points with the given weights. -/
theorem affineCombination_eq_of_weightedVSub_eq_zero_of_eq_neg_one {w : ι → k} {p : ι → P}
(hw : s.weightedVSub p w = (0 : V)) {i : ι} [DecidablePred (· ≠ i)] (his : i ∈ s) (hwi : w i = -1) :
{x ∈ s | x ≠ i}.affineCombination k p w = p i := by
classical
rw [← @vsub_eq_zero_iff_eq V, ← hw, ← s.affineCombination_sdiff_sub (singleton_subset_iff.2 his),
sdiff_singleton_eq_erase, ← filter_ne']
congr
refine (affineCombination_of_eq_one_of_eq_zero _ _ _ (mem_singleton_self _) ?_ ?_).symm
· simp [hwi]
· simp
