English
Let s be a finite set. A point x belongs to the convex hull of s iff there exists a weight function w on E with w(y) ≥ 0 for y ∈ s and ∑_{y∈s} w(y) = 1, and x is the weighted sum x = ∑_{y∈s} w(y) y.
Русский
Пусть s — конечное множество. Точка x принадлежит выпуклой оболочке s тогда и только тогда, существует весовая функция w: E → R с 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
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 ∧ s.centerMass w id = x := by
rw [Finset.convexHull_eq, Set.mem_setOf_eq]
