le_csSup_iff' — Mathlib

English

For a bounded set s, a ≤ sSup s iff for all b ∈ upperBounds s, a ≤ b.

Русский

Для ограниченного сверху множества s верно: a ≤ sSup s тогда и только тогда для всех b ∈ upperBounds s выполняется a ≤ b.

LaTeX

$$$\text{BddAbove}(s) \Rightarrow a \le sSup(s) \iff \forall b, b \in \text{upperBounds}(s) \rightarrow a \le b$$$

Lean4

theorem le_csSup_iff' {s : Set α} {a : α} (h : BddAbove s) : a ≤ sSup s ↔ ∀ b, b ∈ upperBounds s → a ≤ b :=
  ⟨fun h _ hb => le_trans h (csSup_le' hb), fun hb => hb _ fun _ => le_csSup h⟩

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