feat: version of the extreme value theorem without a non-emptiness as…

…sumption (#9872)

Adapted and generalised from sphere-eversion; I'm just upstreaming it.

Mathlib/Topology/Algebra/Order/Compact.lean

@@ -263,6 +263,17 @@ theorem IsCompact.exists_isMinOn [ClosedIicTopology α] {s : Set β} (hs : IsCom
   rcases (hs.image_of_continuousOn hf).exists_isLeast (ne_s.image f) with ⟨_, ⟨x, hxs, rfl⟩, hx⟩
   exact ⟨x, hxs, ball_image_iff.1 hx⟩
 
+/-- If a continuous function lies strictly above `a` on a compact set,
+  it has a lower bound strictly above `a`. -/
+theorem IsCompact.exists_forall_le' [ClosedIicTopology α] [NoMaxOrder α] {f : β → α}
+    {s : Set β} (hs : IsCompact s) (hf : ContinuousOn f s) {a : α} (hf' : ∀ b ∈ s, a < f b) :
+    ∃ a', a < a' ∧ ∀ b ∈ s, a' ≤ f b := by
+  rcases s.eq_empty_or_nonempty with (rfl | hs')
+  · obtain ⟨a', ha'⟩ := exists_gt a
+    exact ⟨a', ha', fun _ a ↦ a.elim⟩
+  · obtain ⟨x, hx, hx'⟩ := hs.exists_isMinOn hs' hf
+    exact ⟨f x, hf' x hx, hx'⟩
+
 /-- The **extreme value theorem**: a continuous function realizes its minimum on a compact set. -/
 @[deprecated IsCompact.exists_isMinOn]
 theorem IsCompact.exists_forall_le [ClosedIicTopology α] {s : Set β} (hs : IsCompact s)