English
Let f be continuous to a linearly ordered space; if the sublevel {x | f(x0) ≤ f(x)} is bounded for some x0, then f has a global maximum.
Русский
Пусть f непрерывна в линейно упорядоченном пространстве; если уровень ≥ f(x0) ограничен для некоторого x0, то существует глобальный максимум.
LaTeX
$$$\text{Continuous } f \Rightarrow \forall x_0,\; \operatorname{IsBounded}\{x: f(x_0) \le f(x)\} \Rightarrow \exists x,\; \forall y,\; f(y) \le f(x).$$$
Lean4
/-- A version of the **Extreme Value Theorem**: if the set where a continuous function `f`
into a linearly ordered space takes values `≥ f x₀` is bounded for some `x₀`,
then `f` has a global maximum (under suitable topological assumptions).
This is a convenient combination of `Continuous.exists_forall_ge'` and
`Metric.isCompact_of_isClosed_isBounded`. -/
theorem exists_forall_ge_of_isBounded {f : β → α} (hf : Continuous f) (x₀ : β)
(h : Bornology.IsBounded {x : β | f x₀ ≤ f x}) : ∃ x, ∀ y, f y ≤ f x :=
hf.exists_forall_le_of_isBounded (α := αᵒᵈ) x₀ h
