isLUB_csSup — Mathlib

English

If s is nonempty and bounded above, then sSup s is a least upper bound of s.

Русский

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

LaTeX

$$$s \neq \varnothing \land BddAbove(s) \rightarrow IsLUB(s, \mathrm{sSup}(s))$$$

Lean4

theorem isLUB_csSup (ne : s.Nonempty) (H : BddAbove s) : IsLUB s (sSup s) :=
  ⟨fun _ => le_csSup H, fun _ => csSup_le ne⟩

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