isLUB_sSup — Mathlib

English

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

Русский

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

LaTeX

$$$\mathrm{IsLUB}(s, \mathrm{sSup}(s))$$$

Lean4

protected theorem isLUB_sSup (h₁ : s.Nonempty) (h₂ : BddAbove s) : IsLUB s (sSup s) :=
  by
  simp only [sSup_def, dif_pos (And.intro h₁ h₂)]
  apply Classical.choose_spec

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