affineCombination_mem_convexHull — Mathlib

English

The centroid of a finite index set lies in the convex hull of the image set.

Русский

Центроид конечного множества лежит в выпуклой оболочке образов.

LaTeX

$$Centroid w s ∈ convexHull R (range s)$$

Lean4

theorem affineCombination_mem_convexHull {s : Finset ι} {v : ι → E} {w : ι → R} (hw₀ : ∀ i ∈ s, 0 ≤ w i)
    (hw₁ : s.sum w = 1) : s.affineCombination R v w ∈ convexHull R (range v) :=
  by
  rw [affineCombination_eq_centerMass hw₁]
  apply s.centerMass_mem_convexHull hw₀
  · simp [hw₁]
  · simp

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