weightedVSub_weightedVSubVSubWeights

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]

Похожие утверждения