English
A weighted subtraction s.weightedVSub p (weightedVSubVSubWeights k i j) equals the vector difference p_i − p_j.
Русский
Взвешенная подстановка s.weightedVSub p (weightedVSubVSubWeights k i j) равна векторной разности p_i − p_j.
LaTeX
$$$s.weightedVSub p (weightedVSubVSubWeights k i j) = p_i -ᵥ p_j$$$
Lean4
/-- A weighted subtraction with `weightedVSubVSubWeights` gives the result of subtracting the
specified points. -/
@[simp]
theorem weightedVSub_weightedVSubVSubWeights [DecidableEq ι] (p : ι → P) {i j : ι} (hi : i ∈ s) (hj : j ∈ s) :
s.weightedVSub p (weightedVSubVSubWeights k i j) = p i -ᵥ p j := by
rw [weightedVSubVSubWeights, ← affineCombination_vsub, s.affineCombination_affineCombinationSingleWeights k p hi,
s.affineCombination_affineCombinationSingleWeights k p hj]