Commit 2023-06-15 03:08 37e61f4e

View on Github →

feat: port Order.Category.FinBddDistLatCat (#5051)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Category/FinBddDistLatCat.lean

added def FinBddDistLatCat.Iso.mk

added def FinBddDistLatCat.dual

added def FinBddDistLatCat.dualEquiv

added def FinBddDistLatCat.of'

added def FinBddDistLatCat.of

added structure FinBddDistLatCat

added theorem finBddDistLatCat_dual_comp_forget_to_bddDistLatCat