English
If a family is convex independent, a point from the family lies in the convex hull of the image of a subset iff its index lies in the subset.
Русский
При выпуквой независимости семейства точка из семейства принадлежит выпуклой оболочке образа подмножества тогда и только тогда, когда её индекс принадлежит этому подмножеству.
LaTeX
$$$p i \\in \\operatorname{convHull}_{\\mathbb{k}}(p''s) \\;\\Leftrightarrow\\; i \\in s$$$
Lean4
/-- If a family is convex independent, a point in the family is in the convex hull of some of the
points given by a subset of the index type if and only if the point's index is in this subset. -/
@[simp]
protected theorem mem_convexHull_iff {p : ι → E} (hc : ConvexIndependent 𝕜 p) (s : Set ι) (i : ι) :
p i ∈ convexHull 𝕜 (p '' s) ↔ i ∈ s :=
⟨hc _ _, fun hi => subset_convexHull 𝕜 _ (Set.mem_image_of_mem p hi)⟩
