exists_isLUB — Mathlib

English

Let α be a linearly ordered topological space with ClosedIci topology. If s is a nonempty compact subset of α, then s has a maximum element; equivalently there exists x ∈ s which is the least upper bound of s.

Русский

Пусть α — линеаризованное топологическое пространство; пусть s ⊆ α не пусто и компактно. Тогда в s существует максимальный элемент: существует x ∈ s такой, что для всех y ∈ s выполняется y ≤ x.

LaTeX

$$$\exists x\in s\; (\forall y\in s\; y\le x)$$$

Lean4

theorem exists_isLUB [ClosedIciTopology α] {s : Set α} (hs : IsCompact s) (ne_s : s.Nonempty) : ∃ x ∈ s, IsLUB s x :=
  IsCompact.exists_isGLB (α := αᵒᵈ) hs ne_s

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