instIsModularLatticeOrderDual

Mathlib.Order.ModularLattice

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

← MathLib Explorer

English

The order dual of a modular lattice is modular.

Русский

Двойственность порядка сохраняет модульность.

LaTeX

$$$ \\text{IsModularLattice}(\\alpha) \\Rightarrow \\text{IsModularLattice}(\\alpha^{\\mathrm{op}}) $$$

Lean4

instance : IsModularLattice αᵒᵈ :=
  ⟨fun y z xz =>
    le_of_eq
      (by
        rw [inf_comm, sup_comm, eq_comm, inf_comm, sup_comm]
        exact @sup_inf_assoc_of_le α _ _ _ y _ xz)⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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