Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-29 14:39 e1bafaa4

View on Github →

feat(category_theory/limits/shapes/images): some explicit instances of has_image_map (#9977)

Estimated changes

Modified src/category_theory/arrow.lean

added theorem category_theory.arrow.inv_left

added theorem category_theory.arrow.inv_right

Modified src/category_theory/limits/shapes/images.lean

added theorem category_theory.limits.has_image.of_arrow_iso

added def category_theory.limits.image_factorisation.of_arrow_iso

modified theorem category_theory.limits.is_image.fac_lift

added def category_theory.limits.is_image.of_arrow_iso

added def category_theory.limits.mono_factorisation.of_arrow_iso