mathlib documentation

order.category.Semilattice

The categories of semilattices #

This defines SemilatticeSup and SemilatticeInf, the categories of sup-semilattices with a bottom element and inf-semilattices with a top element.

References #

structure SemilatticeSup  :
Type (u+1)

The category of sup-semilattices with a bottom element.

Instances for SemilatticeSup
structure SemilatticeInf  :
Type (u+1)

The category of inf-semilattices with a top element.

Instances for SemilatticeInf
def SemilatticeSup.of (α : Type u_1) [semilattice_sup α] [order_bot α] :

Construct a bundled SemilatticeSup from a semilattice_sup.

Equations
@[simp]
theorem SemilatticeSup.coe_of (α : Type u_1) [semilattice_sup α] [order_bot α] :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
def SemilatticeInf.of (α : Type u_1) [semilattice_inf α] [order_top α] :

Construct a bundled SemilatticeInf from a semilattice_inf.

Equations
@[simp]
theorem SemilatticeInf.coe_of (α : Type u_1) [semilattice_inf α] [order_top α] :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations

Order dual #

def SemilatticeSup.iso.mk {α β : SemilatticeSup} (e : α ≃o β) :
α β

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

Equations
@[simp]

order_dual as a functor.

Equations
@[simp]
def SemilatticeInf.iso.mk {α β : SemilatticeInf} (e : α ≃o β) :
α β

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

Equations

order_dual as a functor.

Equations