exists_isMaxOn — Mathlib

English

Let s ⊆ β be compact and nonempty, and f: β → α be continuous on s. Then there exists x ∈ s such that f(x) is the maximum of f on s.

Русский

Пусть s ⊆ β компактно и непусто, и f: β → α непрерывна на s. Тогда существует x ∈ s такой, что f(x) максимален на s.

LaTeX

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

Lean4

/-- The **extreme value theorem**: a continuous function realizes its maximum on a compact set. -/
theorem exists_isMaxOn [ClosedIciTopology α] {s : Set β} (hs : IsCompact s) (ne_s : s.Nonempty) {f : β → α}
    (hf : ContinuousOn f s) : ∃ x ∈ s, IsMaxOn f s x :=
  IsCompact.exists_isMinOn (α := αᵒᵈ) hs ne_s hf

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