sSup_nonneg' — Mathlib

English

If there exists x in s with 0 ≤ x, then 0 ≤ sSup(s).

Русский

Если в s существует элемент x, не меньше нуля, то 0 ≤ sSup(s).

LaTeX

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

Lean4

/-- As `sSup s = 0` when `s` is a set of reals that's unbounded above, it suffices to show that `s`
contains a nonnegative element to show that `0 ≤ sSup s`. -/
theorem sSup_nonneg' (hs : ∃ x ∈ s, 0 ≤ x) : 0 ≤ sSup s := by
  classical
  obtain ⟨x, hxs, hx⟩ := hs
  exact dite _ (fun h ↦ le_csSup_of_le h hxs hx) fun h ↦ (sSup_of_not_bddAbove h).ge

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