instAssociativeMax_mathlib

Mathlib.Order.Lattice

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

English

Join is associative: (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z).

Русский

Соединение ассоциативно: (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z).

LaTeX

$$$(x) \sqcup (y) \sqcup z = x \sqcup (y \sqcup z)$$$

Lean4

instance : Std.Associative (α := α) (· ⊔ ·) :=
  ⟨sup_assoc⟩

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

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

Разделы

Аффилиация

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