Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-25 00:37 3dd8e4d5

View on Github →

feat(order/category/FinBoolAlg): The category of finite Boolean algebras (#12906) Define FinBoolAlg, the category of finite Boolean algebras.

Estimated changes

Modified src/data/set/lattice.lean

added theorem set.preimage_sInter

Modified src/order/category/BoolAlg.lean

added theorem BoolAlg.coe_to_BoundedDistribLattice

Created src/order/category/FinBoolAlg.lean

added theorem FinBoolAlg.coe_of

added theorem FinBoolAlg.coe_to_BoolAlg

added def FinBoolAlg.dual

added def FinBoolAlg.dual_equiv

added def FinBoolAlg.iso.mk

added def FinBoolAlg.of

added structure FinBoolAlg

added def Fintype_to_FinBoolAlg_op

Modified src/order/category/FinPartialOrder.lean

added theorem FinPartialOrder.coe_to_PartialOrder

Modified src/order/hom/complete_lattice.lean

added theorem complete_lattice_hom.coe_set_preimage

added def complete_lattice_hom.set_preimage

added theorem complete_lattice_hom.set_preimage_apply

added theorem complete_lattice_hom.set_preimage_comp

added theorem complete_lattice_hom.set_preimage_id