sSup_nonpos — Mathlib

English

If every x in s satisfies x ≤ 0, then sSup(s) ≤ 0.

Русский

Если каждый элемент множества s не превосходит ноль, то sSup(s) ≤ 0.

LaTeX

$$$\\forall x \\in s, x \\le 0 \\Rightarrow \\operatorname{sSup}(s) \\le 0$$$

Lean4

/-- As `sSup s = 0` when `s` is an empty set of reals, it suffices to show that all elements of `s`
are nonpositive to show that `sSup s ≤ 0`. -/
theorem sSup_nonpos (hs : ∀ x ∈ s, x ≤ 0) : sSup s ≤ 0 :=
  Real.sSup_le hs le_rfl

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