minCardFinsetOfMemConvexHull — Mathlib

English

The min-cardinal finite subset t of a convex hull contains only elements from the original set.

Русский

Минимальная по кардинальности конечная подмножество оболочки выпуклости состоит только из элементов исходного множества.

LaTeX

$$$\\bigl(\\minCardFinsetOfMemConvexHull(x)\\bigr)\\!\\toSet \\subseteq s.$$$

Lean4

/-- Given a point `x` in the convex hull of a set `s`, this is a finite subset of `s` of minimum
cardinality, whose convex hull contains `x`. -/
noncomputable def minCardFinsetOfMemConvexHull (hx : x ∈ convexHull 𝕜 s) : Finset E :=
  Function.argminOn Finset.card {t | ↑t ⊆ s ∧ x ∈ convexHull 𝕜 (t : Set E)} <| by
    simpa only [convexHull_eq_union_convexHull_finite_subsets s, exists_prop, mem_iUnion] using hx

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