exists_isMaxOn_mem_subset — Mathlib

English

Let s ⊆ t with t compact, then there exists x ∈ s such that sSup(f''s) = f(x).

Русский

Пусть s ⊆ t, t компактно; существует x ∈ s, такое что sSup(f''s) = f(x).

LaTeX

$$$\\exists x \\in s,\\ sSup(f''s)=f(x)$$$

Lean4

theorem exists_isMaxOn_mem_subset [ClosedIciTopology α] {f : β → α} {s t : Set β} {z : β} (ht : IsCompact t)
    (hf : ContinuousOn f t) (hz : z ∈ t) (hfz : ∀ z' ∈ t \ s, f z' < f z) : ∃ x ∈ s, IsMaxOn f t x :=
  let ⟨x, hxt, hfx⟩ := ht.exists_isMaxOn ⟨z, hz⟩ hf
  ⟨x, by_contra fun hxs => (hfz x ⟨hxt, hxs⟩).not_ge (hfx hz), hfx⟩
    -- TODO: we could assume `t ∈ 𝓝ˢ s` (a.k.a. `s ⊆ interior t`) instead of `s ⊆ t` and `IsOpen s`.

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