English
For a closed Ici topology α and s ⊆ β, if s is compact and nonempty and f is continuous on s, then there exists x ∈ s that minimizes f on s (variant with dual order).
Русский
Для замкнутого множества и компактной области существует точка минимума функции на этом множестве.
LaTeX
$$$\exists x\in s\; IsMinOn(f,s,x)$$$
Lean4
/-- The **extreme value theorem**: if a function `f` is continuous on a closed set `s` and it is
smaller than a value in its image away from compact sets, then it has a maximum on this set. -/
theorem exists_isMaxOn' [ClosedIciTopology α] {s : Set β} {f : β → α} (hf : ContinuousOn f s) (hsc : IsClosed s)
{x₀ : β} (h₀ : x₀ ∈ s) (hc : ∀ᶠ x in cocompact β ⊓ 𝓟 s, f x ≤ f x₀) : ∃ x ∈ s, IsMaxOn f s x :=
ContinuousOn.exists_isMinOn' (α := αᵒᵈ) hf hsc h₀ hc
