exists_sInf_image_eq

Mathlib.Topology.Order.Compact

URI: https://scilib.ai/kg/mathlib#IsCompact.exists_sInf_image_eq

← MathLib Explorer

English

There exists x ∈ s such that sInf(f''s) = f(x).

Русский

Существует x ∈ s такое, что sInf(f''s) = f(x).

LaTeX

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

Lean4

theorem exists_sInf_image_eq [ClosedIicTopology α] {s : Set β} (hs : IsCompact s) (ne_s : s.Nonempty) {f : β → α}
    (hf : ContinuousOn f s) : ∃ x ∈ s, sInf (f '' s) = f x :=
  let ⟨x, hxs, hx, _⟩ := hs.exists_sInf_image_eq_and_le ne_s hf
  ⟨x, hxs, hx⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru