English
If s is a finite subset of E, then the convex hull of s equals the set of points x for which there exists a finite-weight representation: there exist weights w on the finite set hs.toFinset with w(y) ≥ 0, ∑ w(y) = 1, and hs.toFinset.centerMass w id = x.
Русский
Если s — конечное подмножество E, то выпуклая оболочка s равна множеству точек x, для которых существует конечная запись по весам: существуют веса w на hs.toFinset, такие что w(y) ≥ 0, ∑ w(y) = 1 и hs.toFinset.centerMass w id = x.
LaTeX
$$$x \in \operatorname{conv}(R, s) \iff \exists w : E \to \mathbb{R}, (\forall y \in hs.toFinset, 0 \le w(y)) \; \wedge \; \sum_{y \in hs.toFinset} w(y) = 1 \; \wedge \; hs.toFinset.centerMass w id = x$$$
Lean4
theorem convexHull_eq {s : Set E} (hs : s.Finite) :
convexHull R s =
{x : E | ∃ w : E → R, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ hs.toFinset, w y = 1 ∧ hs.toFinset.centerMass w id = x} :=
by simpa only [Set.Finite.coe_toFinset, Set.Finite.mem_toFinset, exists_prop] using hs.toFinset.convexHull_eq
