mem_extremePoints_iff_mem_diff_convexHull_diff

English

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

Русский

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

LaTeX

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

Lean4

theorem mem_extremePoints_iff_mem_diff_convexHull_diff (hA : Convex 𝕜 A) :
    x ∈ A.extremePoints 𝕜 ↔ x ∈ A \ convexHull 𝕜 (A \ { x }) := by
  rw [hA.mem_extremePoints_iff_convex_diff, hA.convex_remove_iff_notMem_convexHull_remove, mem_diff]

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