English
For a closed set s and a continuous f, if s is compact and nonempty, there exists x ∈ s with f(x) ≤ f(y) for all y ∈ s.
Русский
Для замкнутого множества s и непрерывной функции f, если s компактно и не пусто, существует x ∈ s такое, что f(x) ≤ f(y) для всех y ∈ s.
LaTeX
$$$\exists x\in s\; \forall y\in s\; f(x)\le f(y)$$$
Lean4
/-- The **extreme value theorem**: if a function `f` is continuous on a closed set `s` and it is
larger than a value in its image away from compact sets, then it has a minimum on this set. -/
theorem exists_isMinOn' [ClosedIicTopology α] {s : Set β} {f : β → α} (hf : ContinuousOn f s) (hsc : IsClosed s)
{x₀ : β} (h₀ : x₀ ∈ s) (hc : ∀ᶠ x in cocompact β ⊓ 𝓟 s, f x₀ ≤ f x) : ∃ x ∈ s, IsMinOn f s x :=
by
rcases (hasBasis_cocompact.inf_principal _).eventually_iff.1 hc with ⟨K, hK, hKf⟩
have hsub : insert x₀ (K ∩ s) ⊆ s := insert_subset_iff.2 ⟨h₀, inter_subset_right⟩
obtain ⟨x, hx, hxf⟩ : ∃ x ∈ insert x₀ (K ∩ s), ∀ y ∈ insert x₀ (K ∩ s), f x ≤ f y :=
((hK.inter_right hsc).insert x₀).exists_isMinOn (insert_nonempty _ _) (hf.mono hsub)
refine ⟨x, hsub hx, fun y hy => ?_⟩
by_cases hyK : y ∈ K
exacts [hxf _ (Or.inr ⟨hyK, hy⟩), (hxf _ (Or.inl rfl)).trans (hKf ⟨hyK, hy⟩)]
