mathlib3 documentation

order.category.BoolAlg

The category of boolean algebras #

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

This defines BoolAlg, the category of boolean algebras.

@[protected, instance]
Equations
def BoolAlg.of (α : Type u_1) [boolean_algebra α] :

Construct a bundled BoolAlg from a boolean_algebra.

Equations
@[simp]
theorem BoolAlg.coe_of (α : Type u_1) [boolean_algebra α] :

Turn a BoolAlg into a BddDistLat by forgetting its complement operation.

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

Constructs an equivalence between Boolean algebras from an order isomorphism between them.

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

order_dual as a functor.

Equations