English
An indexed family is convex independent if each member cannot be expressed as a convex combination of other members unless the index is itself included in the index set.
Русский
Указанная семейство индексов является конвексивной независимой, если каждый её элемент не может быть выражен как выпуклая комбинация остальных без включения соответствующего индекса в множество индексов.
LaTeX
$$$\\text{ConvexIndependent}_{\\mathbb{k}}(p) \\;\\coloneqq\\; \\forall (s:\\,\\text{Set }\\,\\iota)(x:\\,\\iota), p(x) \\in \\operatorname{convHull}_{\\mathbb{k}}(p''s) \\Rightarrow x \\in s$$$
Lean4
/-- An indexed family is said to be convex independent if every point only belongs to convex hulls
of sets containing it. -/
def ConvexIndependent (p : ι → E) : Prop :=
∀ (s : Set ι) (x : ι), p x ∈ convexHull 𝕜 (p '' s) → x ∈ s
