Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.
Compact Straszewicz theorem #
This module assembles the compact finite-dimensional Straszewicz theorem from the source-shaped
pieces in ConvexHull and SupportingBall.
theorem
AleksandrovDifferentiability.straszewiczCompactConvexStatement
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
[FiniteDimensional ℝ E]
:
Finite-dimensional compact-convex Straszewicz theorem.
Every extreme point of a compact convex set is a limit of exposed points. The proof follows the
Rockafellar source route: assume an extreme point is not in the exposed-point closure, separate it
from conv (closure exposedPoints), then use the supporting-ball construction to find an exposed
point on the wrong side of the separating halfspace.