Commit 2023-06-14 15:16 b01598d3

View on Github →

feat: port Order.Category.BddLatCat (#5007)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Category/BddLatCat.lean

added def BddLatCat.Iso.mk

added theorem BddLatCat.coe_forget_to_bddOrd

added theorem BddLatCat.coe_forget_to_latCat

added theorem BddLatCat.coe_forget_to_semilatInf

added theorem BddLatCat.coe_forget_to_semilatSup

added theorem BddLatCat.coe_of

added def BddLatCat.dual

added def BddLatCat.dualEquiv

added theorem BddLatCat.forget_latCat_partOrdCat_eq_forget_bddOrd_partOrdCat

added theorem BddLatCat.forget_semilatInf_partOrdCat_eq_forget_bddOrd_partOrdCat

added theorem BddLatCat.forget_semilatSup_partOrdCat_eq_forget_bddOrd_partOrdCat

added def BddLatCat.of

added structure BddLatCat

added theorem bddLatCat_dual_comp_forget_to_bddOrdCat

added theorem bddLatCat_dual_comp_forget_to_latCat

added theorem bddLatCat_dual_comp_forget_to_semilatInfCat

added theorem bddLatCat_dual_comp_forget_to_semilatSupCat

added def latToBddLatCat

added def latToBddLatCatCompDualIsoDualCompLatToBddLatCat

added def latToBddLatCatForgetAdjunction