instIsLowerModularLatticeOrderDual

Mathlib.Order.ModularLattice

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

English

The order dual of an IsUpperModularLattice is IsLowerModularLattice.

Русский

Двойственность OrderDual превращает IsUpperModularLattice в IsLowerModularLattice.

LaTeX

$$$ \\text{IsLowerModularLattice}(\\mathrm{OrderDual}(\\alpha)) \\text{ follows from IsUpperModularLattice}(\\alpha).$$$

Lean4

instance : IsLowerModularLattice (OrderDual α) :=
  ⟨fun h => h.ofDual.sup_of_inf_left.toDual⟩

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

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

Разделы

Аффилиация

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