exists_forall_ge' — Mathlib

English

If a function is continuous on a closed set, and that set is compact and nonempty, then there exists a minimizer on the set.

Русский

Если функция непрерывна на замкнутом множестве и это множество компактно и непусто, существует минимум на множестве.

LaTeX

$$$\exists x\in s\; IsMinOn(f,s,x)$$$

Lean4

/-- The **extreme value theorem**: if a continuous function `f` is smaller than a value in its range
away from compact sets, then it has a global maximum. -/
theorem exists_forall_ge' [ClosedIciTopology α] {f : β → α} (hf : Continuous f) (x₀ : β)
    (h : ∀ᶠ x in cocompact β, f x ≤ f x₀) : ∃ x : β, ∀ y : β, f y ≤ f x :=
  Continuous.exists_forall_le' (α := αᵒᵈ) hf x₀ h

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