English
If a finite collection with weights w_i ≥ 0 and total sum 1 is given along with z_i ∈ s, and the weighted sum equals x, then x lies in convexHull(s).
Русский
Если даны конечная коллекция с весами w_i ≥ 0 и суммой 1, а также z_i ∈ s и суммарная взвешенная сумма равна x, то x ∈ convexHull(s).
LaTeX
$$x ∈ convexHull R s$$
Lean4
/-- Universe polymorphic version of the reverse implication of `mem_convexHull_iff_exists_fintype`.
-/
theorem mem_convexHull_of_exists_fintype {s : Set E} {x : E} [Fintype ι] (w : ι → R) (z : ι → E) (hw₀ : ∀ i, 0 ≤ w i)
(hw₁ : ∑ i, w i = 1) (hz : ∀ i, z i ∈ s) (hx : ∑ i, w i • z i = x) : x ∈ convexHull R s :=
by
rw [← hx, ← centerMass_eq_of_sum_1 _ _ hw₁]
exact centerMass_mem_convexHull _ (by simpa using hw₀) (by simp [hw₁]) (by simpa using hz)
