mathlib3 documentation

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
@[simp]
def FinBddDistLat.iso.mk {α β : FinBddDistLat} (e : α ≃o β) :
α β

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

Equations
@[simp]

order_dual as a functor.

Equations