sSup_def — Mathlib

English

For any s ⊆ ℕ with an upper bound, sSup s is the least upper bound of s.

Русский

Для множества s ⊆ ℕ с верхней границей sSup s есть наименьшее верхнее ограничение множества.

LaTeX

$$$sSup(s) = \min \{ n \\in \mathbb{N} \mid \forall a \\in s, a \\le n \}$$$

Lean4

theorem sSup_def {s : Set ℕ} (h : ∃ n, ∀ a ∈ s, a ≤ n) : sSup s = @Nat.find (fun n ↦ ∀ a ∈ s, a ≤ n) _ h :=
  dif_pos _

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