sInf_nonpos — Mathlib

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⟩

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