Commit 2023-04-14 12:58 71438f76

View on Github →

feat: port CategoryTheory.Limits.Over (#3172)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Over.lean

added theorem CategoryTheory.Over.epi_iff_epi_left

added theorem CategoryTheory.Over.epi_left_of_epi

added def CategoryTheory.Over.mapPullbackAdj

added def CategoryTheory.Over.pullback

added def CategoryTheory.Over.pullbackComp

added def CategoryTheory.Over.pullbackId

added theorem CategoryTheory.Under.mono_iff_mono_right

added theorem CategoryTheory.Under.mono_right_of_mono

added def CategoryTheory.Under.pushout