isLUB_sSup — Mathlib

English

For a nonempty compact set s, the supremum sSup s is the least upper bound (LUB) of s.

Русский

Для непустого компактного множества s верхняя граница sSup s является наименьшей верхней гранью множества.

LaTeX

$$IsLUB(s, sSup s)$$

Lean4

theorem isLUB_sSup [ClosedIciTopology α] {s : Set α} (hs : IsCompact s) (ne_s : s.Nonempty) : IsLUB s (sSup s) :=
  IsCompact.isGLB_sInf (α := αᵒᵈ) hs ne_s

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