isGLB_sInf — Mathlib

English

For a nonempty compact set s, the infimum sInf s is the greatest lower bound (GLB) of s.

Русский

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

LaTeX

$$IsGLB(s, sInf s) (interpreted as: sInf s is the greatest lower bound of s)$$

Lean4

theorem isGLB_sInf [ClosedIicTopology α] {s : Set α} (hs : IsCompact s) (ne_s : s.Nonempty) : IsGLB s (sInf s) :=
  isGLB_csInf ne_s hs.bddBelow

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