inf_comm

Mathlib.Algebra.Order.CauSeq.Basic

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

English

The meet operation is commutative: a ∧ b = b ∧ a for CauSeq elements a and b.

Русский

Найменьшее/меньшее — коммутирует: a ∧ b = b ∧ a.

LaTeX

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

Lean4

protected theorem inf_comm (a b : CauSeq α abs) : a ⊓ b = b ⊓ a :=
  Subtype.ext (inf_comm _ _)

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

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

Разделы

Аффилиация

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