minCardFinsetOfMemConvexHull_subseteq

English

If x lies in convexHull(s), then x lies in convexHull(minCardFinsetOfMemConvexHull x).

Русский

Если x лежит в выпуклой оболочке множества s, тогда x лежит в выпуклой оболочке minCardFinsetOfMemConvexHull x.

LaTeX

$$$x\\in\\operatorname{convexHull}(s)\\Rightarrow x\\in\\operatorname{convexHull}(\\operatorname{minCardFinsetOfMemConvexHull}(x)).$$$

Lean4

theorem minCardFinsetOfMemConvexHull_subseteq : ↑(minCardFinsetOfMemConvexHull hx) ⊆ s :=
  (Function.argminOn_mem _ {t : Finset E | ↑t ⊆ s ∧ x ∈ convexHull 𝕜 (t : Set E)} _).1

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