csSup_pair

Mathlib.Order.ConditionallyCompleteLattice.Basic

URI: https://scilib.ai/kg/mathlib#csSup_pair

English

The supremum of two elements equals their lattice join: sSup {a, b} = a ⊔ b.

Русский

Наибольшая верхняя граница двух элементов равна их объединению: sSup {a, b} = a ⊔ b.

LaTeX

$$$\forall a,b:\\alpha,\ sSup\{a,b\} = a \sqcup b$$$

Lean4

theorem csSup_pair (a b : α) : sSup { a, b } = a ⊔ b :=
  (@isLUB_pair _ _ a b).csSup_eq (insert_nonempty _ _)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru