convexIndependent_extremePoints — Mathlib

English

A variant of the finite-subset criterion for convex independence using finsets.

Русский

Вариант критерия выпуквой независимости через конечные множества.

LaTeX

$$$\\text{ConvexIndependent}_{\\mathbb{k}}(p) \\iff \\forall s : Finset ι, \\; \\forall x:\\iota, p x ∈ convHull_{\\mathbb{k}}(Finset.image\,p\,s).toSet \\Rightarrow x ∈ s$$$

Lean4

theorem convexIndependent_extremePoints (hs : Convex 𝕜 s) : ConvexIndependent 𝕜 ((↑) : s.extremePoints 𝕜 → E) :=
  convexIndependent_set_iff_notMem_convexHull_diff.2 fun _ hx h =>
    (extremePoints_convexHull_subset
          (inter_extremePoints_subset_extremePoints_of_subset
            (convexHull_min (Set.diff_subset.trans extremePoints_subset) hs) ⟨h, hx⟩)).2
      (Set.mem_singleton _)

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