affineCombination_vsub — Mathlib

English

Equality of affine combinations is preserved under map and precomposition with an embedding; i.e., maps of affine combinations correspond.

Русский

Сохранение равенства аффинной комбинации при отображении и предварительном вложении.

LaTeX

$$$\text{affineCombination map compatibility: } \,$$$

Lean4

/-- Subtracting two `affineCombination`s. -/
theorem affineCombination_vsub (w₁ w₂ : ι → k) (p : ι → P) :
    s.affineCombination k p w₁ -ᵥ s.affineCombination k p w₂ = s.weightedVSub p (w₁ - w₂) := by
  rw [← AffineMap.linearMap_vsub, affineCombination_linear, vsub_eq_sub]

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