mathlib3 documentation

order.category.CompleteLat

The category of complete lattices #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines CompleteLat, the category of complete lattices.

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

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

Equations
@[simp]
theorem CompleteLat.iso.mk_hom {α β : CompleteLat} (e : α ≃o β) :

order_dual as a functor.

Equations