instIsWeakUpperModularLatticeOrderDual

English

The dual of IsLowerModularLattice is IsUpperModularLattice on the order dual.

Русский

Двойственность IsLowerModularLattice даёт IsUpperModularLattice на OrderDual.

LaTeX

$$$ \\text{IsUpperModularLattice}(\\mathrm{OrderDual}(\\alpha)) \ \\,\\text{если } \\alpha \\text{ имеет IsLowerModularLattice}.$$$

Lean4

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

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