exists_sSup_image_eq

Mathlib.Topology.Order.Compact

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

theorem exists_sSup_image_eq [ClosedIciTopology α] {s : Set β} (hs : IsCompact s) (ne_s : s.Nonempty) :
    ∀ {f : β → α}, ContinuousOn f s → ∃ x ∈ s, sSup (f '' s) = f x :=
  IsCompact.exists_sInf_image_eq (α := αᵒᵈ) hs ne_s

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

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

Разделы

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

Аффилиация

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