le_sInf — Mathlib

English

If all x in s satisfy a ≤ x and a ≤ 0, then a ≤ sInf(s).

Русский

Если для всех x ∈ s выполняется a ≤ x и a ≤ 0, то a ≤ sInf(s).

LaTeX

$$$\\forall x \\in s, a \\le x \\quad\\land\\quad a \\le 0 \\Rightarrow a \\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 at least some nonpositive number `a` to show that `a ≤ sInf s`.

See also `le_csInf`. -/
protected theorem le_sInf (hs : ∀ x ∈ s, a ≤ x) (ha : a ≤ 0) : a ≤ sInf s :=
  by
  obtain rfl | hs' := s.eq_empty_or_nonempty
  exacts [ha.trans_eq sInf_empty.symm, le_csInf hs' hs]

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