mathlib documentation

order.category.CompleteLattice

The category of complete lattices #

This file defines CompleteLattice, the category of complete lattices.

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

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

Equations

order_dual as a functor.

Equations