affineCombination_linear — Mathlib

English

The linear part of the affine combination map equals the weightedVSub operator, i.e., (s.affineCombination k p).linear = s.weightedVSub p.

Русский

Линейная часть отображения аффинной комбинации равна оператору weightedVSub; т.е. (s.affineCombination k p).linear = s.weightedVSub p.

LaTeX

$$$ (s.affineCombination\ k\ p).linear = s.weightedVSub\ p $$$

Lean4

/-- The linear map corresponding to `affineCombination` is
`weightedVSub`. -/
@[simp]
theorem affineCombination_linear (p : ι → P) : (s.affineCombination k p).linear = s.weightedVSub p :=
  rfl

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