mathlib

8150c5eb - feat(category_theory/morphism_property): miscellaneous basic results (#16444)

feat(category_theory/morphism_property): miscellaneous basic results (#16444) This PR establishes miscellaneous results about `morphism_property` in category theory: how `stable_under_composition`, etc, behave with passing to the opposite category, the definition of the inverse image of a `morphism_property` by a functor, the definition of isomorphisms/monomorphisms/epimorphisms as morphism properties.