English
A continuous affine map sends extreme points of a compact set onto extreme points of the image; more precisely, it induces a surjection from extremePoints(s) onto extremePoints(f''s).
Русский
Непрерывное аффинное отображение переводит экстремальные точки множества в экстремальные точки образа; по существу оно образует сюрьекцию extremePoints(s) на extremePoints(f''s).
LaTeX
$$$\\operatorname{SurjOn} f (\\operatorname{extremePoints}_{\\mathbb{R}}(s)) (\\operatorname{extremePoints}_{\\mathbb{R}}(f''s)).$$$
Lean4
/-- **Krein-Milman theorem**: In a LCTVS, any compact convex set is the closure of the convex hull
of its extreme points. -/
theorem closure_convexHull_extremePoints (hscomp : IsCompact s) (hAconv : Convex ℝ s) :
closure (convexHull ℝ <| s.extremePoints ℝ) = s :=
by
apply (closure_minimal (convexHull_min extremePoints_subset hAconv) hscomp.isClosed).antisymm
by_contra hs
obtain ⟨x, hxA, hxt⟩ := not_subset.1 hs
obtain ⟨l, r, hlr, hrx⟩ := geometric_hahn_banach_closed_point (convex_convexHull _ _).closure isClosed_closure hxt
have h : IsExposed ℝ s ({y ∈ s | ∀ z ∈ s, l z ≤ l y}) := fun _ => ⟨l, rfl⟩
obtain ⟨z, hzA, hz⟩ := hscomp.exists_isMaxOn ⟨x, hxA⟩ l.continuous.continuousOn
obtain ⟨y, hy⟩ := (h.isCompact hscomp).extremePoints_nonempty ⟨z, hzA, hz⟩
linarith [hlr _ (subset_closure <| subset_convexHull _ _ <| h.isExtreme.extremePoints_subset_extremePoints hy),
hy.1.2 x hxA]
