Commit 2023-03-08 20:49 0f2df18d

View on Github →

feat: port CategoryTheory.Limits.Shapes.NormalMono.Basic (#2732)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Shapes/NormalMono/Basic.lean

added def CategoryTheory.NormalEpi.desc'

added def CategoryTheory.NormalMono.lift'

added def CategoryTheory.equivalenceReflectsNormalEpi

added def CategoryTheory.equivalenceReflectsNormalMono

added def CategoryTheory.normalEpiOfEpi

added def CategoryTheory.normalEpiOfNormalMonoUnop

added def CategoryTheory.normalMonoOfMono

added def CategoryTheory.normalMonoOfNormalEpiUnop

added def CategoryTheory.normalOfIsPullbackFstOfNormal

added def CategoryTheory.normalOfIsPullbackSndOfNormal

added def CategoryTheory.normalOfIsPushoutFstOfNormal

added def CategoryTheory.normalOfIsPushoutSndOfNormal