Extreme points of sublevel-compact sets

Convex-analysis facts supplementing Mathlib's extreme-point / Krein-Milman API, built towards: the infimum of a linear functional over a closed convex set is attained at an extreme point of the set, given a known compact sublevel set.

theorem exists_isMinOn_of_isCompact_sublevel {F : Type u_1} [TopologicalSpace F] {s : Set F} {l : F → ℝ} (hl : ContinuousOn l s) {x₀ : F} (hx₀ : x₀ ∈ s) (hK : IsCompact {y : F | y ∈ s ∧ l y ≤ l x₀}) : ∃ x ∈ s, IsMinOn l s x

If l is continuous on s and has a compact sublevel set {y ∈ s | l y ≤ l x₀} at some x₀ ∈ s, then l attains its minimum over all of s.

theorem isExposed_setOf_isMinOn {F : Type u_1} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] (l : StrongDual ℝ F) (s : Set F) : IsExposed ℝ s {y : F | y ∈ s ∧ IsMinOn (⇑l) s y}

The set of minimizers of a continuous linear functional over s is an exposed subset of s.

theorem isExtreme_setOf_isMinOn {F : Type u_1} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] (l : StrongDual ℝ F) (s : Set F) : IsExtreme ℝ s {y : F | y ∈ s ∧ IsMinOn (⇑l) s y}

The set of minimizers of a continuous linear functional is an extreme subset of s.

theorem isCompact_setOf_isMinOn {F : Type u_1} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] (l : StrongDual ℝ F) {s : Set F} {x₀ : F} (hx₀ : x₀ ∈ s) (hK : IsCompact {y : F | y ∈ s ∧ l y ≤ l x₀}) : IsCompact {y : F | y ∈ s ∧ IsMinOn (⇑l) s y}

The set of minimizers of a continuous linear functional is compact, given a compact sublevel set at some x₀ ∈ s.

theorem exists_extremePoint_isMinOn {F : Type u_1} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [T2Space F] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] [LocallyConvexSpace ℝ F] (l : StrongDual ℝ F) {s : Set F} {x₀ : F} (hx₀ : x₀ ∈ s) (hK : IsCompact {y : F | y ∈ s ∧ l y ≤ l x₀}) : ∃ x ∈ Set.extremePoints ℝ s, IsMinOn (⇑l) s x

Layer 1 capstone: In an LCTVS, if l is a continuous linear functional on a set s with a compact sublevel set at some x₀ ∈ s, then the minimum of l over s is attained at an extreme point of s.