English
If f is continuous on a closed set s and s is compact and nonempty, there exists x ∈ s attaining the maximum of f on s.
Русский
Если f непрерывна на замкнутом множестве s и s компактно и не пусто, существует x ∈ s достигающий максимум функции f на s.
LaTeX
$$$\exists x\in s\; IsMaxOn(f,s,x)$$$
Lean4
/-- The **extreme value theorem**: if a continuous function `f` is larger than a value in its range
away from compact sets, then it has a global minimum. -/
theorem exists_forall_le' [ClosedIicTopology α] {f : β → α} (hf : Continuous f) (x₀ : β)
(h : ∀ᶠ x in cocompact β, f x₀ ≤ f x) : ∃ x : β, ∀ y : β, f x ≤ f y :=
let ⟨x, _, hx⟩ := hf.continuousOn.exists_isMinOn' isClosed_univ (mem_univ x₀) (by rwa [principal_univ, inf_top_eq])
⟨x, fun y => hx (mem_univ y)⟩
