English
Let s ⊆ β be compact and nonempty, and f: β → α be continuous on s. Then there exists x ∈ s such that f(x) is the minimum of f on s.
Русский
Пусть s ⊆ β компактно и непусто, и f: β → α непрерывна на s. Тогда существует x ∈ s, такой что f(x) минимально на s.
LaTeX
$$$\exists x\in s\; IsMinOn(f,s,x)$$$
Lean4
/-- If a continuous function lies strictly above `a` on a compact set,
it has a lower bound strictly above `a`. -/
theorem exists_forall_le' [ClosedIicTopology α] [NoMaxOrder α] {f : β → α} {s : Set β} (hs : IsCompact s)
(hf : ContinuousOn f s) {a : α} (hf' : ∀ b ∈ s, a < f b) : ∃ a', a < a' ∧ ∀ b ∈ s, a' ≤ f b :=
by
rcases s.eq_empty_or_nonempty with (rfl | hs')
· obtain ⟨a', ha'⟩ := exists_gt a
exact ⟨a', ha', fun _ a ↦ a.elim⟩
· obtain ⟨x, hx, hx'⟩ := hs.exists_isMinOn hs' hf
exact ⟨f x, hf' x hx, hx'⟩
