English
Every point in the convex hull can be expressed as an affine combination of finitely many points from the set.
Русский
Каждая точка в выпуклой оболочке может быть выражена как аффинная комбинация конечного числа точек множества.
LaTeX
$$convexHull R s = {x | ∃ (ι) (t : Finset ι) (w : ι → R) (z : ι → E), (∀ i ∈ t, 0 ≤ w i) ∧ ∑ i ∈ t, w i = 1 ∧ ∀ i ∈ t, z i ∈ s ∧ t.centerMass w z = x}$$
Lean4
theorem centroid_mem_convexHull (s : Finset E) (hs : s.Nonempty) : s.centroid R id ∈ convexHull R (s : Set E) :=
by
rw [s.centroid_eq_centerMass hs]
apply s.centerMass_id_mem_convexHull
· simp only [inv_nonneg, imp_true_iff, Nat.cast_nonneg, Finset.centroidWeights_apply]
· have hs_card : (#s : R) ≠ 0 := by simp [Finset.nonempty_iff_ne_empty.mp hs]
simp only [hs_card, Finset.sum_const, nsmul_eq_mul, mul_inv_cancel₀, Ne, not_false_iff,
Finset.centroidWeights_apply, zero_lt_one]
