English
If s is a compact subset of β and f is continuous on s, then there exists x ∈ s minimizing f on s.
Русский
Пусть s — компактное подмножество β и f непрерывна на s. Тогда существует x ∈ s, минимизирующий f на s.
LaTeX
$$$\exists x\in s\; IsMinOn(f,s,x)$$$
Lean4
/-- The **extreme value theorem**: a continuous function realizes its minimum on a compact set. -/
theorem exists_isMinOn [ClosedIicTopology α] {s : Set β} (hs : IsCompact s) (ne_s : s.Nonempty) {f : β → α}
(hf : ContinuousOn f s) : ∃ x ∈ s, IsMinOn f s x :=
by
rcases (hs.image_of_continuousOn hf).exists_isLeast (ne_s.image f) with ⟨_, ⟨x, hxs, rfl⟩, hx⟩
refine ⟨x, hxs, forall_mem_image.1 (fun _ hb => hx <| mem_image_of_mem f ?_)⟩
rwa [(image_id' s).symm]
