instIsModularLattice

Mathlib.Order.ModularLattice

URI: https://scilib.ai/kg/mathlib#DistribLattice.instIsModularLattice

English

A distributive lattice is modular; thus any DistribLattice α inherits IsModularLattice.

Русский

Дистрибутивная решетка модульна; значит, DistribLattice α наследует IsModularLattice.

LaTeX

$$$[\DistribLattice \alpha]\Rightarrow IsModularLattice \alpha.$$$

Lean4

instance (priority := 100) [DistribLattice α] : IsModularLattice α :=
  ⟨fun y z xz => by rw [inf_sup_right, inf_eq_left.2 xz]⟩

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

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

Разделы

Аффилиация

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