English
If f is a linear equivalence, then the image of the extreme points of s under f equals the extreme points of the image of s.
Русский
Если f — линейное эквивалентное отображение, то образ крайних точек s под действием f совпадает с крайними точками образа s.
LaTeX
$$$f '' \operatorname{extremePoints}_{𝕜} s = \operatorname{extremePoints}_{𝕜} (f '' s)$$$
Lean4
theorem image_extremePoints (f : L) (s : Set E) : f '' extremePoints 𝕜 s = extremePoints 𝕜 (f '' s) :=
by
ext b
obtain ⟨a, rfl⟩ := EquivLike.surjective f b
have : ∀ x y, f '' openSegment 𝕜 x y = openSegment 𝕜 (f x) (f y) :=
image_openSegment _ (LinearMapClass.linearMap f).toAffineMap
simp only [mem_extremePoints, (EquivLike.surjective f).forall, (EquivLike.injective f).mem_set_image,
(EquivLike.injective f).eq_iff, ← this]
