sSup_pair — Mathlib

English

Let a, b be elements of a complete lattice. Then the supremum of the two-element set {a, b} equals their join a ⊔ b.

Русский

Пусть a, b — элементы полной решётки. Тогда верхняя граница множества {a, b} равна их объединению a ⊔ b.

LaTeX

$$$$ \operatorname{sSup} \{ a, b \} = a \sqcup b $$$$

Lean4

theorem sSup_pair {a b : α} : sSup { a, b } = a ⊔ b :=
  (@isLUB_pair α _ a b).sSup_eq

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