English
Let s be a finite subset of E. The membership x ∈ conv_R(s) is equivalent to the existence of a weight function w on E such that w(y) ≥ 0 for all y ∈ s, ∑_{y∈s} w(y) = 1, and x = ∑_{y∈s} w(y) y.
Русский
Пусть s — конечное подмножество E. Членство x в выпуклой оболочке s эквивалентно существованию весовой функции w на E такая что w(y) ≥ 0 для y ∈ s, ∑_{y∈s} w(y) = 1 и x = ∑_{y∈s} w(y) y.
LaTeX
$$$x \in \operatorname{conv}(R, (s : Set E)) \iff \exists w : E \to \mathbb{R}, (\forall y \in s, 0 \le w(y)) \; \wedge \; \sum_{y \in s} w(y) = 1 \; \wedge \; \sum_{y \in s} w(y) \; y = x$$$
Lean4
/-- This is a version of `Finset.mem_convexHull` stated without `Finset.centerMass`. -/
theorem mem_convexHull' {s : Finset E} {x : E} :
x ∈ convexHull R (s : Set E) ↔ ∃ w : E → R, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ ∑ y ∈ s, w y • y = x :=
by
rw [mem_convexHull]
refine exists_congr fun w ↦ and_congr_right' <| and_congr_right fun hw ↦ ?_
simp_rw [centerMass_eq_of_sum_1 _ _ hw, id_eq]
