exists_forall_ge — Mathlib

English

For a continuous function on a compact set, there exists a global minimum on the set.

Русский

Для непрерывной функции на компактном множестве существует глобальный минимум на этом множестве.

LaTeX

$$$\exists x\in s\; \forall y\in s\; f(x) \le f(y)$$$

Lean4

/-- The **extreme value theorem**: if a continuous function `f` tends to negative infinity away from
compact sets, then it has a global maximum. -/
theorem exists_forall_ge [ClosedIciTopology α] [Nonempty β] {f : β → α} (hf : Continuous f)
    (hlim : Tendsto f (cocompact β) atBot) : ∃ x, ∀ y, f y ≤ f x :=
  Continuous.exists_forall_le (α := αᵒᵈ) hf hlim

Похожие утверждения