mem_extremePoints_iff_convex_diff

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 mem_extremePoints_iff_convex_diff (hA : Convex 𝕜 A) : x ∈ A.extremePoints 𝕜 ↔ x ∈ A ∧ Convex 𝕜 (A \ { x }) :=
  by
  use fun hx ↦ ⟨hx.1, (isExtreme_singleton.2 hx).convex_diff hA⟩
  rintro ⟨hxA, hAx⟩
  refine mem_extremePoints_iff_forall_segment.2 ⟨hxA, fun x₁ hx₁ x₂ hx₂ hx ↦ ?_⟩
  rw [convex_iff_segment_subset] at hAx
  by_contra! h
  exact (hAx ⟨hx₁, fun hx₁ ↦ h.1 (mem_singleton_iff.2 hx₁)⟩ ⟨hx₂, fun hx₂ ↦ h.2 (mem_singleton_iff.2 hx₂)⟩ hx).2 rfl

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