affineCombination_eq_centerMass — Mathlib

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]

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