instIsWeakLowerModularLatticeOrderDual

English

The order dual of a lattice with IsWeakUpperModularLattice becomes IsWeakLowerModularLattice.

Русский

Обратная по порядку множества структура решётки с IsWeakUpperModularLattice становится IsWeakLowerModularLattice.

LaTeX

$$$ \text{If } \\alpha \text{ is a lattice and IsWeakUpperModularLattice } \\alpha, \\text{ then } IsWeakLowerModularLattice (\\mathrm{OrderDual}(\\alpha)).$$$

Lean4

instance : IsWeakLowerModularLattice (OrderDual α) :=
  ⟨fun ha hb => (ha.ofDual.sup_of_inf_of_inf_left hb.ofDual).toDual⟩

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