sInf_nonpos' — Mathlib

English

If there exists x ∈ s with x ≤ 0, then sInf(s) ≤ 0.

Русский

Если существует x ∈ s такое, что x ≤ 0, то sInf(s) ≤ 0.

LaTeX

$$$\\exists 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 unbounded below, it suffices to show that `s`
contains a nonpositive element to show that `sInf s ≤ 0`. -/
theorem sInf_nonpos' (hs : ∃ x ∈ s, x ≤ 0) : sInf s ≤ 0 := by
  classical
  obtain ⟨x, hxs, hx⟩ := hs
  exact dite _ (fun h ↦ csInf_le_of_le h hxs hx) fun h ↦ (sInf_of_not_bddBelow h).le

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