exists_sInf_image_eq_and_le — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem exists_sInf_image_eq_and_le [ClosedIicTopology α] {s : Set β} (hs : IsCompact s) (ne_s : s.Nonempty) {f : β → α}
    (hf : ContinuousOn f s) : ∃ x ∈ s, sInf (f '' s) = f x ∧ ∀ y ∈ s, f x ≤ f y :=
  let ⟨x, hxs, hx⟩ := (hs.image_of_continuousOn hf).sInf_mem (ne_s.image f)
  ⟨x, hxs, hx.symm, fun _y hy =>
    hx.trans_le <| csInf_le (hs.image_of_continuousOn hf).bddBelow <| mem_image_of_mem f hy⟩

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