csSup_mem — Mathlib

English

If s is nonempty and bounded above, then the supremum of s belongs to s.

Русский

Если множество непусто и ограничено сверху, то его супремум принадлежит этому множеству.

LaTeX

$$$\operatorname{sSup}(s) \in s$$$

Lean4

theorem csSup_mem {s : Set ℤ} (h1 : s.Nonempty) (h2 : BddAbove s) : sSup s ∈ s :=
  by
  convert (greatestOfBdd _ (Classical.choose_spec h2) h1).2.1
  exact dif_pos ⟨h1, h2⟩

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