instSupSet — Mathlib

English

The real numbers admit a supremum operation: for any nonempty set s bounded above, there exists a real sSup s which is the least upper bound of s.

Русский

В вещественных число существует операция верхней гранни: для любого непустого множества s, ограниченного сверху, существует его верхняя грань sSup s — наименьшая верхняя грань множества s.

LaTeX

$$$IsLUB(s, sSup(s))$$$

Lean4

noncomputable instance : SupSet ℝ :=
  ⟨fun s => if h : s.Nonempty ∧ BddAbove s then Classical.choose (exists_isLUB h.1 h.2) else 0⟩

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