inf_inf_inf_comm

Mathlib.Order.Lattice

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

English

a Ⓧ b Ⓧ (c Ⓧ d) = a Ⓧ c Ⓧ (b Ⓧ d) for all a,b,c,d.

Русский

a ⊓ b ⊓ (c ⊓ d) = a ⊓ c ⊓ (b ⊓ d) для всех a,b,c,d.

LaTeX

$$$ \forall a,b,c,d,\ a \wedge b \wedge (c \wedge d) = a \wedge c \wedge (b \wedge d) $$$

Lean4

theorem inf_inf_inf_comm (a b c d : α) : a ⊓ b ⊓ (c ⊓ d) = a ⊓ c ⊓ (b ⊓ d) :=
  @sup_sup_sup_comm αᵒᵈ _ _ _ _ _

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

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

Разделы

Аффилиация

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