exists_forall_le — Mathlib

English

If f is continuous and tends to infinity outside a cocompact region, then f attains a global minimum on the region.

Русский

Если f непрерывна и убывает к бесконечности вне коккомпактной области, то достигается глобальный минимум на этой области.

LaTeX

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

Lean4

/-- The **extreme value theorem**: if a continuous function `f` tends to infinity away from compact
sets, then it has a global minimum. -/
theorem exists_forall_le [ClosedIicTopology α] [Nonempty β] {f : β → α} (hf : Continuous f)
    (hlim : Tendsto f (cocompact β) atTop) : ∃ x, ∀ y, f x ≤ f y :=
  by
  inhabit β
  exact hf.exists_forall_le' default (hlim.eventually <| eventually_ge_atTop _)

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