sum_smul_const_vsub_eq_vsub_affineCombination

English

An alternative formulation of affineCombination_map where the embedding is reorganized; the equality holds with composed arguments accordingly.

Русский

Альтернативная формулировка равенства affineCombination_map, где вложение реорганизовано; равенство сохраняется при композициях аргументов.

LaTeX

$$$$ \text{(описание эквивалентной формы)} $$$$

Lean4

/-- A weighted sum of pairwise subtractions, where the point on the left is constant and the
sum of the weights is 1. -/
theorem sum_smul_const_vsub_eq_vsub_affineCombination (w : ι → k) (p₂ : ι → P) (p₁ : P) (h : ∑ i ∈ s, w i = 1) :
    (∑ i ∈ s, w i • (p₁ -ᵥ p₂ i)) = p₁ -ᵥ s.affineCombination k p₂ w := by
  rw [sum_smul_vsub_eq_affineCombination_vsub, affineCombination_apply_const _ _ _ h]

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