# Documentation

Mathlib.Order.Category.CompleteLat

# The category of complete lattices #

This file defines CompleteLat, the category of complete lattices.

def CompleteLat :
Type (u_1 + 1)

The category of complete lattices.

Equations
Instances For
def CompleteLat.of (α : Type u_1) [] :

Construct a bundled CompleteLat from a CompleteLattice.

Equations
Instances For
@[simp]
theorem CompleteLat.coe_of (α : Type u_1) [] :
() = α
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem CompleteLat.Iso.mk_inv_toFun {α : CompleteLat} {β : CompleteLat} (e : α ≃o β) (a : β) :
.inv a = () a
@[simp]
theorem CompleteLat.Iso.mk_hom_toFun {α : CompleteLat} {β : CompleteLat} (e : α ≃o β) (a : α) :
.hom a = e a
def CompleteLat.Iso.mk {α : CompleteLat} {β : CompleteLat} (e : α ≃o β) :
α β

Constructs an isomorphism of complete lattices from an order isomorphism between them.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CompleteLat.dual_map {X : CompleteLat} {Y : CompleteLat} (a : ) :
CompleteLat.dual.map a = CompleteLatticeHom.dual a

OrderDual as a functor.

Equations
Instances For

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

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