# mathlibdocumentation

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.

structure BoundedLattice  :
Type (u_1+1)

The category of bounded lattices with bounded lattice morphisms.

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

Construct a bundled BoundedLattice from lattice + bounded_order.

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

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

Equations
@[simp]

order_dual as a functor.

Equations
@[simp]
theorem BoundedLattice.dual_map (X Y : BoundedLattice) (ᾰ : Y) :

The equivalence between BoundedLattice and itself induced by order_dual both ways.

Equations