sSup_mem — Mathlib

English

If s is a nonempty compact subset and f attains its maximum on s, then sSup s belongs to the image and is achieved by some x ∈ s.

Русский

Для непустого компактного множества s и функции f, достигающей максимума на s, точка достижения максимума существует в s.

LaTeX

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

Lean4

theorem sSup_mem [ClosedIciTopology α] {s : Set α} (hs : IsCompact s) (ne_s : s.Nonempty) : sSup s ∈ s :=
  IsCompact.sInf_mem (α := αᵒᵈ) hs ne_s

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