sInf_nonneg — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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