exists_isLocalMin_mem_open — Mathlib

English

For a nonempty compact s, sInf s is the greatest lower bound of s.

Русский

Для непустого компактного множества s sInf s является наибольшей нижней гранью множества.

LaTeX

$$IsGLB(s, sInf s)$$

Lean4

theorem exists_isLocalMin_mem_open [ClosedIicTopology α] {f : β → α} {s t : Set β} {z : β} (ht : IsCompact t)
    (hst : s ⊆ t) (hf : ContinuousOn f t) (hz : z ∈ t) (hfz : ∀ z' ∈ t \ s, f z < f z') (hs : IsOpen s) :
    ∃ x ∈ s, IsLocalMin f x :=
  let ⟨x, hxs, h⟩ := ht.exists_isMinOn_mem_subset hf hz hfz
  ⟨x, hxs, h.isLocalMin <| mem_nhds_iff.2 ⟨s, hst, hs, hxs⟩⟩

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