English
Same principle as above for a continuous affine map; the image of extreme points covers all extreme points of the image set.
Русский
То же самое для непрерывного аффинного отображения: образ экстремальных точек покрывает все экстремальные точки образа.
LaTeX
$$$\\operatorname{SurjOn} f (\\operatorname{extremePoints}_{\\mathbb{R}}(s)) (\\operatorname{extremePoints}_{\\mathbb{R}}(f''s)).$$$
Lean4
/-- A continuous affine map is surjective from the extreme points of a compact set to the extreme
points of the image of that set. This inclusion is in general strict. -/
theorem surjOn_extremePoints_image (f : E →ᴬ[ℝ] F) (hs : IsCompact s) :
SurjOn f (extremePoints ℝ s) (extremePoints ℝ (f '' s)) :=
by
rintro w hw
have ht : IsCompact ({x ∈ s | f x = w}) := hs.inter_right <| isClosed_singleton.preimage f.continuous
have ht₀ : {x ∈ s | f x = w}.Nonempty := by simpa using extremePoints_subset hw
obtain ⟨x, ⟨hx, rfl⟩, hyt⟩ := ht.extremePoints_nonempty ht₀
refine mem_image_of_mem _ ⟨hx, fun y hy z hz hxyz ↦ ?_⟩
have := by simpa using image_openSegment _ f.toAffineMap y z
rw [mem_extremePoints] at hw
have := hw.2 _ (mem_image_of_mem _ hy) _ (mem_image_of_mem _ hz) <| by rw [← this]; exact mem_image_of_mem _ hxyz
exact hyt ⟨hy, this.1⟩ ⟨hz, this.2⟩ hxyz
