Commit 2023-02-22 04:23 fe496b79

View on Github →

feat: port CategoryTheory.Limits.Shapes.StrongEpi (#2327)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Shapes/StrongEpi.lean

added theorem CategoryTheory.StrongEpi.iff_of_arrow_iso

added theorem CategoryTheory.StrongEpi.mk'

added theorem CategoryTheory.StrongEpi.of_arrow_iso

added theorem CategoryTheory.StrongMono.iff_of_arrow_iso

added theorem CategoryTheory.StrongMono.mk'

added theorem CategoryTheory.StrongMono.of_arrow_iso

added theorem CategoryTheory.isIso_of_epi_of_strongMono

added theorem CategoryTheory.isIso_of_mono_of_strongEpi

added theorem CategoryTheory.strongEpi_comp

added theorem CategoryTheory.strongEpi_of_epi

added theorem CategoryTheory.strongEpi_of_strongEpi

added theorem CategoryTheory.strongMono_comp

added theorem CategoryTheory.strongMono_of_mono

added theorem CategoryTheory.strongMono_of_strongMono