Commit 2023-03-07 14:15 eaca0de1

View on Github →

feat: port CategoryTheory.Limits.Shapes.RegularMono (#2686)

Estimated changes

Modified Mathlib.lean

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

added def CategoryTheory.RegularEpi.desc'

added def CategoryTheory.RegularMono.lift'

added theorem CategoryTheory.isIso_of_regularEpi_of_mono

added theorem CategoryTheory.isIso_of_regularMono_of_epi

added def CategoryTheory.regularEpiOfEpi

added def CategoryTheory.regularMonoOfMono

added def CategoryTheory.regularOfIsPullbackFstOfRegular

added def CategoryTheory.regularOfIsPullbackSndOfRegular

added def CategoryTheory.regularOfIsPushoutFstOfRegular

added def CategoryTheory.regularOfIsPushoutSndOfRegular