mathlib3

c10a8728 - feat(order): define a `rel_hom_class` for types of relation-preserving maps (#10755)

feat(order): define a `rel_hom_class` for types of relation-preserving maps (#10755) Use the design of #9888 to define a class `rel_hom_class F r s` for types of maps such that all `f : F` satisfy `r a b → s (f a) (f b)`. Requested by @YaelDillies. `order_hom_class F α β` is defined as an abbreviation for `rel_hom_class F (≤) (≤)`.