sSup_le — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- As `sSup s = 0` when `s` is an empty set of reals, it suffices to show that all elements of `s`
are at most some nonnegative number `a` to show that `sSup s ≤ a`.

See also `csSup_le`. -/
protected theorem sSup_le (hs : ∀ x ∈ s, x ≤ a) (ha : 0 ≤ a) : sSup s ≤ a :=
  by
  obtain rfl | hs' := s.eq_empty_or_nonempty
  exacts [sSup_empty.trans_le ha, csSup_le hs' hs]

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