mathlib documentation

order.category.DistribLattice

The category of distributive lattices #

This file defines DistribLattice, the category of distributive lattices.

Note that DistLat in the literature doesn't always correspond to DistribLattice as we don't require bottom or top elements. Instead, this DistLat corresponds to BoundedDistribLattice.

@[protected, instance]
Equations
def DistribLattice.of (α : Type u_1) [distrib_lattice α] :

Construct a bundled DistribLattice from a distrib_lattice underlying type and typeclass.

Equations
@[simp]
theorem DistribLattice.coe_of (α : Type u_1) [distrib_lattice α] :
def DistribLattice.iso.mk {α β : DistribLattice} (e : α ≃o β) :
α β

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

Equations
@[simp]

order_dual as a functor.

Equations