exists_sSup_image_eq_and_ge — Mathlib

English

For a nonempty compact set s and continuous On f on s, there exists x ∈ s with sSup(f''s) = f(x) and f(x) is maximal on s.

Русский

Для непустого компактного множества s и непрерывной на s функции f существует x ∈ s, такое что sSup(f''s)=f(x) и f(x) максимальное на s.

LaTeX

$$$\\exists x\\in s,\\ sSup(f''s)=f(x)\\,\\land\\,\\forall y\\in s, f(y)\\le f(x)$$$

Lean4

theorem exists_sSup_image_eq_and_ge [ClosedIciTopology α] {s : Set β} (hs : IsCompact s) (ne_s : s.Nonempty) {f : β → α}
    (hf : ContinuousOn f s) : ∃ x ∈ s, sSup (f '' s) = f x ∧ ∀ y ∈ s, f y ≤ f x :=
  IsCompact.exists_sInf_image_eq_and_le (α := αᵒᵈ) hs ne_s hf

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