English
Let f be continuous to a linearly ordered space; if the sublevel set {x | f(x) ≤ f(x0)} is bounded for some x0, then f has a global minimum.
Русский
Пусть f непрерывна и принимает значения в линейно упорядоченном пространстве; если уровень ≤ f(x0) ограничен для некоторого x0, то f достигает глобального минимума.
LaTeX
$$$\text{Continuous } f \Rightarrow \forall x_0,\; \operatorname{IsBounded}\{x: f(x) \le f(x_0)\} \Rightarrow \exists x,\; \forall y,\; f(x) \le f(y).$$$
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 minimum (under suitable topological assumptions).
This is a convenient combination of `Continuous.exists_forall_le'` and
`Metric.isCompact_of_isClosed_isBounded`. -/
theorem exists_forall_le_of_isBounded {f : β → α} (hf : Continuous f) (x₀ : β)
(h : Bornology.IsBounded {x : β | f x ≤ f x₀}) : ∃ x, ∀ y, f x ≤ f y :=
by
refine hf.exists_forall_le' (x₀ := x₀) ?_
have hU : {x : β | f x₀ < f x} ∈ Filter.cocompact β :=
by
refine Filter.mem_cocompact'.mpr ⟨_, ?_, fun ⦃_⦄ a ↦ a⟩
simp only [Set.compl_setOf, not_lt]
exact Metric.isCompact_of_isClosed_isBounded (isClosed_le (by fun_prop) (by fun_prop)) h
filter_upwards [hU] with x hx using hx.le
