Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-20 06:10 34db3c34

View on Github →

feat(order/category): various categories of ordered types (#3841) This is a first step towards the category of simplicial sets (which are presheaves on the category of nonempty finite linear orders).

Estimated changes

added def Preorder.of
added def Preorder
added theorem preorder_hom.coe_id
added theorem preorder_hom.coe_inj
added theorem preorder_hom.comp_id
added theorem preorder_hom.ext
added def preorder_hom.id
added theorem preorder_hom.id_comp
added structure preorder_hom