isLeast_csInf — Mathlib

English

If s is closed, nonempty and bounded below, then sInf s is the least element of s with respect to the order.

Русский

Если s замкнуто, непусто и ограничено снизу, то sInf s является наименьшим элементом s относительно порядка.

LaTeX

$$$IsClosed(s) \land s.Nonempty \land BddBelow(s) \Rightarrow IsLeast(s, sInf(s))$$$

Lean4

theorem isLeast_csInf {s : Set α} (hc : IsClosed s) (hs : s.Nonempty) (B : BddBelow s) : IsLeast s (sInf s) :=
  ⟨hc.csInf_mem hs B, (isGLB_csInf hs B).1⟩

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