English
Exposed relation implies extreme relation: IsExposed 𝕜 A B ⇒ IsExtreme 𝕜 A B.
Русский
Экспонированность множества A относительно B следует из того, что A и B образуют крайние множества.
LaTeX
$$$$ IsExposed\ 𝕜 A B \Rightarrow IsExtreme\ 𝕜 A B. $$$$
Lean4
protected theorem isExtreme (hAB : IsExposed 𝕜 A B) : IsExtreme 𝕜 A B :=
by
refine ⟨hAB.subset, fun x₁ hx₁A x₂ hx₂A x hxB hx => ?_⟩
obtain ⟨l, rfl⟩ := hAB ⟨x, hxB⟩
have hl : ConvexOn 𝕜 univ l := l.toLinearMap.convexOn convex_univ
have hlx₁ := hxB.2 x₁ hx₁A
have hlx₂ := hxB.2 x₂ hx₂A
refine ⟨hx₁A, fun y hy => ?_⟩
rw [hlx₁.antisymm (hl.le_left_of_right_le (mem_univ _) (mem_univ _) hx hlx₂)]
exact hxB.2 y hy
