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
/-- A useful restatement using `segment`: `x` is an extreme point iff the only (closed) segments
that contain it are those with `x` as one of their endpoints. -/
theorem mem_extremePoints_iff_forall_segment :
x ∈ A.extremePoints 𝕜 ↔ x ∈ A ∧ ∀ᵉ (x₁ ∈ A) (x₂ ∈ A), x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x :=
by
rw [mem_extremePoints]
refine and_congr_right fun hxA ↦ forall₄_congr fun x₁ h₁ x₂ h₂ ↦ ?_
constructor
· rw [← insert_endpoints_openSegment]
rintro H (rfl | rfl | hx)
exacts [Or.inl rfl, Or.inr rfl, Or.inl <| (H hx).1]
· intro H hx
rcases H (openSegment_subset_segment _ _ _ hx) with (rfl | rfl)
exacts [⟨rfl, (left_mem_openSegment_iff.1 hx).symm⟩, ⟨right_mem_openSegment_iff.1 hx, rfl⟩]
