sSup_mem — Mathlib

English

If s ≠ ∅ and BddAbove s, then sSup s ∈ s.

Русский

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

LaTeX

$$$\\forall s \\subseteq \\mathbb{N}, s \\neq \emptyset \land \\text{BddAbove}(s) \\Rightarrow sSup(s) \\in s$$$

Lean4

theorem sSup_mem {s : Set ℕ} (h₁ : s.Nonempty) (h₂ : BddAbove s) : sSup s ∈ s :=
  let ⟨k, hk⟩ := h₂
  h₁.csSup_mem ((finite_le_nat k).subset hk)

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