exists_isMinOn_mem_subset — Mathlib

English

Let s ⊆ t with t compact and s compact, then there exists x ∈ s with sInf (f''s) ≤ f x.

Русский

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

LaTeX

$$$\\exists x \\in s,\\ sInf(f''s) \\le f(x)$$$

Lean4

theorem exists_isMinOn_mem_subset [ClosedIicTopology α] {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, IsMinOn f t x :=
  let ⟨x, hxt, hfx⟩ := ht.exists_isMinOn ⟨z, hz⟩ hf
  ⟨x, by_contra fun hxs => (hfz x ⟨hxt, hxs⟩).not_ge (hfx hz), hfx⟩

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