# mathlib3documentation

order.category.FinBddDistLat

# The category of finite bounded distributive lattices #

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

This file defines FinBddDistLat, the category of finite distributive lattices with bounded lattice homomorphisms.

structure FinBddDistLat  :
Type (u_1+1)

The category of finite distributive lattices with bounded lattice morphisms.

Instances for FinBddDistLat
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
def FinBddDistLat.of (α : Type u_1) [fintype α] :

Construct a bundled FinBddDistLat from a nonempty bounded_order distrib_lattice.

Equations
def FinBddDistLat.of' (α : Type u_1) [fintype α] [nonempty α] :

Construct a bundled FinBddDistLat from a nonempty bounded_order distrib_lattice.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem FinBddDistLat.iso.mk_hom {α β : FinBddDistLat} (e : α ≃o β) :
def FinBddDistLat.iso.mk {α β : FinBddDistLat} (e : α ≃o β) :
α β

Constructs an equivalence between finite distributive lattices from an order isomorphism between them.

Equations
@[simp]
theorem FinBddDistLat.iso.mk_inv {α β : FinBddDistLat} (e : α ≃o β) :
= (e.symm)
@[simp]
@[simp]

order_dual as a functor.

Equations

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

Equations
@[simp]
@[simp]