extremePoints_convexHull_subset — Mathlib

English

The extreme points of the convex hull of A are contained in A.

Русский

Крайние точки выпуклой оболочки A содержатся в A.

LaTeX

$$$\operatorname{extremePoints}_{𝕜}(\operatorname{convexHull}_{𝕜} A) \subseteq A$$$

Lean4

theorem extremePoints_convexHull_subset : (convexHull 𝕜 A).extremePoints 𝕜 ⊆ A :=
  by
  rintro x hx
  rw [(convex_convexHull 𝕜 _).mem_extremePoints_iff_convex_diff] at hx
  by_contra h
  exact (convexHull_min (subset_diff.2 ⟨subset_convexHull 𝕜 _, disjoint_singleton_right.2 h⟩) hx.2 hx.1).2 rfl

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