English
If every x ∈ s satisfies x ≤ 0, then sInf(s) ≤ 0.
Русский
Если каждый x ∈ s удовлетворяет x ≤ 0, то sInf(s) ≤ 0.
LaTeX
$$$\\forall x \\in s, x \\le 0 \\Rightarrow \\operatorname{sInf}(s) \\le 0$$$
Lean4
/-- As `sInf s = 0` when `s` is a set of reals that's either empty or unbounded below,
it suffices to show that all elements of `s` are nonpositive to show that `sInf s ≤ 0`. -/
theorem sInf_nonpos (hs : ∀ x ∈ s, x ≤ 0) : sInf s ≤ 0 :=
by
obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
· exact sInf_empty.le
· exact sInf_nonpos' ⟨x, hx, hs _ hx⟩