sSup_of_not_bddAbove — Mathlib

English

Let S be a subset of NNReal that is not bounded above. Then the supremum of S is 0.

Русский

Пусть S ⊆ ℝ≥0 не ограничено сверху. Тогда его супремум равен 0.

LaTeX

$$$ \text{If } S \subseteq \mathbb{R}_{\ge 0} \text{ is unbounded above, then } \sup S = 0.$$$

Lean4

nonrec theorem sSup_of_not_bddAbove {s : Set ℝ≥0} (hs : ¬BddAbove s) : SupSet.sSup s = 0 := by
  grind [csSup_of_not_bddAbove, csSup_empty, bot_eq_zero']

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