Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-18 16:15 c10a8728

View on Github →

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 (≤) (≤).

Estimated changes

modified theorem order_hom.ext
added def order_hom_class
modified theorem rel_embedding.ext
modified theorem rel_embedding.ext_iff
modified theorem rel_hom.coe_fn_injective
deleted theorem rel_hom.map_inf
deleted theorem rel_hom.map_rel
deleted theorem rel_hom.map_sup
added theorem rel_hom_class.map_inf
added theorem rel_hom_class.map_sup
modified theorem rel_iso.coe_fn_injective
modified theorem rel_iso.ext
modified theorem rel_iso.ext_iff