English
Affine combination of points preserves membership in the convex hull via the center mass representation.
Русский
Аффинная комбинация точек сохраняет принадлежность выпуклому оболочке через представление центра массы.
LaTeX
$$s.affineCombination R p w ∈ convexHull R (range p)$$
Lean4
theorem affineCombination_eq_centerMass {ι : Type*} {t : Finset ι} {p : ι → E} {w : ι → R} (hw₂ : ∑ i ∈ t, w i = 1) :
t.affineCombination R p w = centerMass t w p :=
by
rw [affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ w _ hw₂ (0 : E), Finset.weightedVSubOfPoint_apply,
vadd_eq_add, add_zero, t.centerMass_eq_of_sum_1 _ hw₂]
simp_rw [vsub_eq_sub, sub_zero]