sup_comm

Mathlib.Algebra.Order.CauSeq.Basic

URI: https://scilib.ai/kg/mathlib#CauSeq.sup_comm

English

The join operation is commutative: a ⊔ b = b ⊔ a for CauSeq elements a and b.

Русский

Сумма верхних пределов ний коммутативна: a ⊔ b = b ⊔ a для CauSeq.

LaTeX

$$$\forall a,b \in \mathrm{CauSeq}(\alpha, \mathrm{abs}),\; a \vee b = b \vee a$$$

Lean4

protected theorem sup_comm (a b : CauSeq α abs) : a ⊔ b = b ⊔ a :=
  Subtype.ext (sup_comm _ _)

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

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

Разделы

Аффилиация

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