exists_isLocalMax_mem_open — Mathlib

English

sInf s is the least element of s, i.e., the minimum exists in s.

Русский

sInf s является наименьшим элементом множества s; следовательно, минимум существует в s.

LaTeX

$$IsLeast s (sInf s)$$

Lean4

theorem exists_isLocalMax_mem_open [ClosedIciTopology α] {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, IsLocalMax f x :=
  let ⟨x, hxs, h⟩ := ht.exists_isMaxOn_mem_subset hf hz hfz
  ⟨x, hxs, h.isLocalMax <| mem_nhds_iff.2 ⟨s, hst, hs, hxs⟩⟩

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