csSup_le_iff' — Mathlib

English

For a set s bounded above, sSup s ≤ a if and only if every x ∈ s satisfies x ≤ a.

Русский

Для множества s, ограниченного сверху, sSup s ≤ a тогда и только тогда, когда каждый элемент x ∈ s удовлетворяет x ≤ a.

LaTeX

$$$\text{BddAbove}(s) \Rightarrow \bigl(sSup(s) \le a \iff \forall x \in s, x \le a\bigr)$$$

Lean4

/-- In conditionally complete orders with a bottom element, the nonempty condition can be omitted
from `csSup_le_iff`. -/
theorem csSup_le_iff' {s : Set α} (hs : BddAbove s) {a : α} : sSup s ≤ a ↔ ∀ x ∈ s, x ≤ a :=
  isLUB_le_iff (isLUB_csSup' hs)

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