affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one

English

Two affine combinations are equal if their weights and point families are equal on the finite set s.

Русский

Две аффинные комбинации равны, если их веса и семейства точек совпадают на конечном наборе s.

LaTeX

$$$ s.affineCombination k p_1 w_1 = s.affineCombination k p_2 w_2 \text{ if } \forall i\in s, w_1(i)=w_2(i)\text{ and } \forall i\in s, p_1(i)=p_2(i). $$$

Lean4

/-- `affineCombination` gives the sum with any base point, when the
sum of the weights is 1. -/
theorem affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one (w : ι → k) (p : ι → P) (h : ∑ i ∈ s, w i = 1)
    (b : P) : s.affineCombination k p w = s.weightedVSubOfPoint p b w +ᵥ b :=
  s.weightedVSubOfPoint_vadd_eq_of_sum_eq_one w p h _ _

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