Analysis · existing Mathlib declaration

Krein–Milman Theorem

In a real Hausdorff locally convex topological vector space, a compact convex set is completely recovered by taking all convex combinations of its extreme points and then taking the closure. The closure matters: this statement does not reduce the set to a finite polytope or promise a finite representation of each point.

compact convex sets
extreme points
closed convex hull
locally convex spaces
geometric Hahn–Banach separation
exposed faces

The theorem at a glance

Krein–Milman Theorem at a glance

A source-bound editorial overview of the exact Mathlib formulation. The image is explanatory; the statement map, formal type, and pinned source remain authoritative.

An ivory convex-analysis poster states that a compact convex set in a real Hausdorff locally convex topological vector space equals the closure of the convex hull of its extreme points, then diagrams the separating-functional and exposed-face contradiction. — Compact convex sets in real Hausdorff locally convex spaces are the closed convex hulls of their extreme points.

Formal orientation

Statement map

This deterministic map orients the reader from the mathematical summary to the pinned declaration and exact checked form. The HTML statement below is authoritative.

A dense family of gold extreme points runs around the entire boundary of K, dense convex-combination chords fill its interior, and closure recovers the filled body K. — A compact convex set is the closure of the convex hull of its full set of extreme points.

Complementary intuition

A mathematical landmark

Krein–Milman is a cornerstone of infinite-dimensional convexity: it says that compact convex structure is controlled by extreme points, while the necessary closure records the genuinely topological content. Mathlib's proof exposes the central Hahn–Banach separation and extreme-face architecture.

The low-text schematic gives the theorem a visual identity; it does not replace the source-bound poster or exact statement.

Authoritative formal type

Exact Mathlib statement

theorem closure_convexHull_extremePoints {E : Type*} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [T2Space E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {s : Set E} (hscomp : IsCompact s) (hAconv : Convex ℝ s) : closure (convexHull ℝ (s.extremePoints ℝ)) = s

Selected evidence declaration text

theorem closure_convexHull_extremePoints {E : Type*} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [T2Space E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {s : Set E} (hscomp : IsCompact s) (hAconv : Convex ℝ s) : closure (convexHull ℝ (s.extremePoints ℝ)) = s

ProofAtlas record

What has been checked

Upstream indexedPinned source bytes verified locally

Locally reproducedExact upstream declaration replayed

Reviewed pageCurrent public presentation reviewed

Accepted Atlas resultNot recorded for the preferred artifact

These states distinguish upstream identity, local reproduction, review, and Atlas acceptance. This page is part of the public, read-only Mathlib landmark collection.

Claim boundary

No new theorem is claimed

This page indexes Mathlib's Krein–Milman theorem in a real Hausdorff locally convex topological vector space: every compact convex set s equals closure (convexHull ℝ (s.extremePoints ℝ)). No finite-dimensional hypothesis is present, and the closure is part of the formal conclusion. The set may be empty. The selected declaration does not supply a finite convex representation, a bound on the number of extreme points, or the finite-dimensional strengthening in which closure can sometimes be removed.

The closure in closure (convexHull ℝ (s.extremePoints ℝ)) is part of the theorem and is not removed.
The declaration does not assume finite dimension or prove a finite-dimensional strengthening.
It does not assert that the set of extreme points is finite or that every point has a finite or uniformly bounded extreme-point representation.
It does not extend the equality to arbitrary noncompact convex sets.
ProofAtlas did not originate the theorem or Mathlib's declaration, and the generated explanation and visuals are not proof evidence.

Provenance

Origin and evidence stay separate

Existing declaration: closure_convexHull_extremePoints in mathlib
Relationship: The checked artifact is the upstream declaration itself
Preferred checked artifact: artifact.library.mathlib.krein-milman-theorem.v001
Source handling: Verified upstream reference; no mirrored source package