English
A convex independent family cannot have a point belonging to the convex hull of the rest, i.e., p i ∉ convHull(p''(s\\{i})) for all i.
Русский
Конвексивно независимое семейство не содержит точку, лежащую в выпуклой оболочке остальных, то есть $p_i\\notin \\operatorname{convHull}(p''(s\\{i\\}))$ для всех $i$.
LaTeX
$$$\\text{ConvexIndependent}_{\\mathbb{k}}(p) \\iff \\forall i\\; \\forall s,\\; p i \\notin convHull_{\\mathbb{k}}(p''(s \\setminus \\{i\\})).$$$
Lean4
/-- If a family is convex independent, a point in the family is not in the convex hull of the other
points. See `convexIndependent_set_iff_notMem_convexHull_diff` for the `Set` version. -/
theorem convexIndependent_iff_notMem_convexHull_diff {p : ι → E} :
ConvexIndependent 𝕜 p ↔ ∀ i s, p i ∉ convexHull 𝕜 (p '' (s \ { i })) :=
by
refine ⟨fun hc i s h => ?_, fun h s i hi => ?_⟩
· rw [hc.mem_convexHull_iff] at h
exact h.2 (Set.mem_singleton _)
· by_contra H
refine h i s ?_
rw [Set.diff_singleton_eq_self H]
exact hi
