Commit 2023-06-14 20:11 b75e0092

View on Github →

feat: port Order.Category.BddDistLatCat (#5015)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Category/BddDistLatCat.lean

added def BddDistLatCat.Iso.mk

added theorem BddDistLatCat.coe_of

added theorem BddDistLatCat.coe_toBddLat

added def BddDistLatCat.dual

added def BddDistLatCat.dualEquiv

added theorem BddDistLatCat.forget_bddLat_latCat_eq_forget_distLatCat_latCat

added def BddDistLatCat.of

added def BddDistLatCat.toBddLat

added structure BddDistLatCat

added theorem bddDistLatCat_dual_comp_forget_to_distLatCat