mathlib documentation

order.category.BoundedLattice

The category of bounded lattices #

This file defines BoundedLattice, the category of bounded lattices.

In literature, this is sometimes called Lat, the category of lattices, because being a lattice is understood to entail having a bottom and a top element.

@[protected, instance]
Equations
def BoundedLattice.of (α : Type u_1) [lattice α] [bounded_order α] :

Construct a bundled BoundedLattice from lattice + bounded_order.

Equations
@[simp]
theorem BoundedLattice.coe_of (α : Type u_1) [lattice α] [bounded_order α] :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
def BoundedLattice.iso.mk {α β : BoundedLattice} (e : α ≃o β) :
α β

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

Equations

order_dual as a functor.

Equations