isLUB_sSup — Mathlib

English

Let α be a complete partial order. If a subset d ⊆ α is directed with respect to ≤, then sSup d is the least upper bound of d.

Русский

Пусть α — полная частично упорядоченная множество. Если подмножество d ⊆ α направлено относительно ≤, то sSup d является наименьшим верхним пределом множества d.

LaTeX

$$$\text{DirectedOn}(\le)\ d \rightarrow \text{IsLUB}(d, sSup\ d)$$$

Lean4

protected theorem isLUB_sSup : DirectedOn (· ≤ ·) d → IsLUB d (sSup d) :=
  CompletePartialOrder.lubOfDirected _

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