le_csSup_iff — Mathlib

English

For a bounded above nonempty set s in a ConditionallyCompleteLattice α, a ≤ sSup(s) iff a ≤ every upper bound of s.

Русский

Для ограниченной сверху непустой множества s в решётке α верно: a ≤ sSup(s) тогда и только тогда, когда a ≤ каждый верхний предел s.

LaTeX

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

Lean4

theorem le_csSup_iff (h : BddAbove s) (hs : s.Nonempty) : a ≤ sSup s ↔ ∀ b, b ∈ upperBounds s → a ≤ b :=
  ⟨fun h _ hb => le_trans h (csSup_le hs hb), fun hb => hb _ fun _ => le_csSup h⟩

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