Commit 2023-02-15 11:33 4ed65899

View on Github →

feat: port CategoryTheory.Category.Preorder (#2206)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Category/Preorder.lean

added def CategoryTheory.Equivalence.toOrderIso

added theorem CategoryTheory.Equivalence.toOrderIso_apply

added theorem CategoryTheory.Equivalence.toOrderIso_symm_apply

added theorem CategoryTheory.Functor.monotone

added theorem CategoryTheory.Iso.to_eq

added def CategoryTheory.homOfLE

added theorem CategoryTheory.hom_of_le_comp

added theorem CategoryTheory.hom_of_le_le_of_hom

added theorem CategoryTheory.hom_of_le_refl

added theorem CategoryTheory.leOfHom

added theorem CategoryTheory.le_ofOp_hom

added theorem CategoryTheory.le_of_hom_hom_of_le

added def CategoryTheory.opHomOfLe

added def Monotone.functor

added theorem Monotone.functor_obj