English
A point lies in the convex hull of s if and only if it can be expressed as a finite affine combination of points from s.
Русский
Точка находится в выпуклой оболочке множества s тогда и только тогда, когда её можно выразить через конечную аффинную комбинацию точек из s.
LaTeX
$$x ∈ convexHull R s \Leftrightarrow ∃ (ι) (_ : Fintype ι) (w : ι → R) (z : ι → E), (∀ i, 0 ≤ w i) ∧ ∑ i, w i = 1 ∧ (∀ i, z i ∈ s) ∧ ∑ i, w i • z i = x$$
Lean4
/-- The convex hull of `s` is equal to the set of centers of masses of finite families of points in
`s`.
For universe reasons, you shouldn't use this lemma to prove that a given center of mass belongs
to the convex hull. Use `mem_convexHull_of_exists_fintype` of the convex hull instead. -/
theorem mem_convexHull_iff_exists_fintype {s : Set E} {x : E} :
x ∈ convexHull R s ↔
∃ (ι : Type) (_ : Fintype ι) (w : ι → R) (z : ι → E),
(∀ i, 0 ≤ w i) ∧ ∑ i, w i = 1 ∧ (∀ i, z i ∈ s) ∧ ∑ i, w i • z i = x :=
by
constructor
· simp only [convexHull_eq, mem_setOf_eq]
rintro ⟨ι, t, w, z, h⟩
refine ⟨t, inferInstance, w ∘ (↑), z ∘ (↑), ?_⟩
simpa [← sum_attach t, centerMass_eq_of_sum_1 _ _ h.2.1] using h
· rintro ⟨ι, _, w, z, hw₀, hw₁, hz, hx⟩
exact mem_convexHull_of_exists_fintype w z hw₀ hw₁ hz hx
