weightedVSub_vadd_affineCombination

English

Adding a weightedVSub to an affineCombination corresponds to adding the weight vectors and combining the results.

Русский

Сложение weightedVSub и affineCombination соответствует объединению весов и получению нового результата.

LaTeX

$$$ s.weightedVSub(p,w_1) +_v s.affineCombination(k,p,w_2) = s.affineCombination(k,p, w_1+w_2) $$$

Lean4

/-- Adding a `weightedVSub` to an `affineCombination`. -/
theorem weightedVSub_vadd_affineCombination (w₁ w₂ : ι → k) (p : ι → P) :
    s.weightedVSub p w₁ +ᵥ s.affineCombination k p w₂ = s.affineCombination k p (w₁ + w₂) := by
  rw [← vadd_eq_add, AffineMap.map_vadd, affineCombination_linear]

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