convexIndependent — Mathlib

English

If the index set has at most one element, any indexed family is convex independent.

Русский

Если множество индексов состоит не более чем из одного элемента, любая соответствующая семейство выпукво независима.

LaTeX

$$$[\\text{Subsingleton }\\iota] \\;\\Rightarrow\\; \\text{ConvexIndependent}_{\\mathbb{k}}(p),$$$

Lean4

/-- A family with at most one point is convex independent. -/
theorem convexIndependent [Subsingleton ι] (p : ι → E) : ConvexIndependent 𝕜 p :=
  by
  intro s x hx
  have : (convexHull 𝕜 (p '' s)).Nonempty := ⟨p x, hx⟩
  rw [convexHull_nonempty_iff, Set.image_nonempty] at this
  rwa [Subsingleton.mem_iff_nonempty]

Похожие утверждения