le_csSup — Mathlib

English

If s is bounded above, then every a ∈ s with a ≥ all elements of s satisfies a ≤ sSup s.

Русский

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

LaTeX

$$$$ \text{If } BddAbove(s) \text{ and } a \in s, \ and\ a \le sSup(s) $$$$

Lean4

theorem le_csSup (h₁ : BddAbove s) (h₂ : a ∈ s) : a ≤ sSup s :=
  ConditionallyCompleteLattice.le_csSup s a h₁ h₂

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