sup_inf_sup_assoc

Mathlib.Order.ModularLattice

URI: https://scilib.ai/kg/mathlib#IsModularLattice.sup_inf_sup_assoc

English

In a modular lattice, the identity (x ∨ z) ∧ (y ∨ z) = (x ∧ y) ∨ z holds in dual forms.

Русский

В модульной решётке выполняется двойственный аналог (x ∨ z) ∧ (y ∨ z) = (x ∧ y) ∨ z.

LaTeX

$$$ (x \\lor z) \\land (y \\lor z) = (x \\land y) \\lor z $$$

Lean4

theorem sup_inf_sup_assoc : (x ⊔ z) ⊓ (y ⊔ z) = (x ⊔ z) ⊓ y ⊔ z :=
  @IsModularLattice.inf_sup_inf_assoc αᵒᵈ _ _ _ _ _

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

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

Разделы

Аффилиация

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