Extreme points of (strictly convex) sets

This file collects some results of extreme points of (strictly convex) sets.

Main results

• disjoint_interior_extremePoints: the interior and extreme points of a set in a nontrivial topological vector space are disjoint.
• StrictConvex.sdiff_interior_subset_extremePoints: when C is a strictly convex set then C \ interior C ⊆ extremePoints 𝕜 C.
• StrictConvex.extremePoints_eq_sdiff_interior: the extreme points of a strictly convex set S in nontrivial normed space is exactly S \ interior S.

Corollaries of the above is that, in a nontrivial normed space, the extreme points of the closed ball is contained in the sphere (see extremePoints_closedBall_subset_sphere). And in a nontrivial strictly convex space, the extreme points of the closed ball is exactly the sphere (see StrictConvexSpace.extremePoints_closedBall_eq_sphere).

theorem disjoint_interior_extremePoints {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [Nontrivial E] (S : Set E) : Disjoint (interior S) (Set.extremePoints ℝ S)

theorem StrictConvex.sdiff_interior_subset_extremePoints {𝕜 : Type u_1} {A : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid A] [Module 𝕜 A] [TopologicalSpace A] {C : Set A} (hc : StrictConvex 𝕜 C) : C \ interior C ⊆ Set.extremePoints 𝕜 C

@[deprecated StrictConvex.sdiff_interior_subset_extremePoints (since := "2026-06-03")]

theorem StrictConvex.diff_interior_subset_extremePoints {𝕜 : Type u_1} {A : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid A] [Module 𝕜 A] [TopologicalSpace A] {C : Set A} (hc : StrictConvex 𝕜 C) : C \ interior C ⊆ Set.extremePoints 𝕜 C

Alias of StrictConvex.sdiff_interior_subset_extremePoints.

theorem extremePoints_closedBall_subset_sphere {A : Type u_1} [NormedAddCommGroup A] [NormedSpace ℝ A] [Nontrivial A] {x : A} {r : ℝ} : Set.extremePoints ℝ (Metric.closedBall x r) ⊆ Metric.sphere x r

In a nontrivial normed space, the extreme points of the closed ball is contained in the sphere.

theorem StrictConvex.extremePoints_eq_sdiff_interior {A : Type u_1} [NormedAddCommGroup A] [NormedSpace ℝ A] [Nontrivial A] {S : Set A} (hS : StrictConvex ℝ S) : Set.extremePoints ℝ S = S \ interior S

@[deprecated StrictConvex.extremePoints_eq_sdiff_interior (since := "2026-06-03")]

theorem StrictConvex.extremePoints_eq_diff_interior {A : Type u_1} [NormedAddCommGroup A] [NormedSpace ℝ A] [Nontrivial A] {S : Set A} (hS : StrictConvex ℝ S) : Set.extremePoints ℝ S = S \ interior S

Alias of StrictConvex.extremePoints_eq_sdiff_interior.

theorem StrictConvexSpace.sphere_subset_extremePoints_closedBall {A : Type u_1} [NormedAddCommGroup A] [NormedSpace ℝ A] [StrictConvexSpace ℝ A] (a : A) {r : ℝ} (hr : r ≠ 0) : Metric.sphere a r ⊆ Set.extremePoints ℝ (Metric.closedBall a r)

In a strictly convex space, the sphere is contained in the extreme points of the closed ball when the radius is nonzero. In a nontrivial space, they are equal, see extremePoints_closedBall_eq_sphere.

theorem StrictConvexSpace.extremePoints_closedBall_eq_sphere {A : Type u_1} [NormedAddCommGroup A] [NormedSpace ℝ A] [Nontrivial A] {x : A} {r : ℝ} [StrictConvexSpace ℝ A] : Set.extremePoints ℝ (Metric.closedBall x r) = Metric.sphere x r

@[simp]

theorem Set.extremePoints_Icc {a b : ℝ} (hab : a ≤ b) : extremePoints ℝ (Icc a b) = {a, b}