Documentation

Mathlib.Order.Category.BddDistLat

The category of bounded distributive lattices #

This defines BddDistLat, the category of bounded distributive lattices.

Note that this category is sometimes called DistLat when being a lattice is understood to entail having a bottom and a top element.

structure BddDistLat :
Type (u_1 + 1)

The category of bounded distributive lattices with bounded lattice morphisms.

Instances For

    Construct a bundled BddDistLat from a BoundedOrder DistribLattice.

    Equations
    Instances For
      @[simp]
      theorem BddDistLat.coe_of (α : Type u_1) [DistribLattice α] [BoundedOrder α] :

      Turn a BddDistLat into a BddLat by forgetting it is distributive.

      Equations
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.

        Constructs an equivalence between bounded distributive lattices from an order isomorphism between them.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          OrderDual as a functor.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            The equivalence between BddDistLat and itself induced by OrderDual both ways.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For