isLeast_sInf — Mathlib

English

For a nonempty compact set s, the supremum sSup s is the greatest element of s in the order sense.

Русский

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

LaTeX

$$IsGreatest(s, sSup s)$$

Lean4

theorem isLeast_sInf [ClosedIicTopology α] {s : Set α} (hs : IsCompact s) (ne_s : s.Nonempty) : IsLeast s (sInf s) :=
  ⟨hs.sInf_mem ne_s, (hs.isGLB_sInf ne_s).1⟩

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