English
Same as above with a set version, linking memberwise condition to subset relations.
Русский
То же самое в версии для множества: членство в выпуклой оболочке эквивалентно подмножеству индексов.
LaTeX
$$$\\text{ConvexIndependent}_{\\mathbb{k}}((\\uparrow):s\\to E) \\Leftrightarrow \\forall x\\in s, x\\in s \\Rightarrow \\text{Not}(\\cdot)$$$
Lean4
/-- If a set is convex independent, a point in the set is not in the convex hull of the other
points. See `convexIndependent_iff_notMem_convexHull_diff` for the indexed family version. -/
theorem convexIndependent_set_iff_notMem_convexHull_diff {s : Set E} :
ConvexIndependent 𝕜 ((↑) : s → E) ↔ ∀ x ∈ s, x ∉ convexHull 𝕜 (s \ { x }) :=
by
rw [convexIndependent_set_iff_inter_convexHull_subset]
constructor
· rintro hs x hxs hx
exact (hs _ Set.diff_subset ⟨hxs, hx⟩).2 (Set.mem_singleton _)
· rintro hs t ht x ⟨hxs, hxt⟩
by_contra h
exact hs _ hxs (convexHull_mono (Set.subset_diff_singleton ht h) hxt)
