Commit 2023-03-10 16:28 e26fd77f

View on Github →

feat: port CategoryTheory.Limits.Comma (#2776)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Comma.lean

added def CategoryTheory.Comma.coconeOfPreserves

added def CategoryTheory.Comma.coconeOfPreservesIsColimit

added def CategoryTheory.Comma.colimitAuxiliaryCocone

added def CategoryTheory.Comma.coneOfPreserves

added def CategoryTheory.Comma.coneOfPreservesIsLimit

added def CategoryTheory.Comma.limitAuxiliaryCone

added theorem CategoryTheory.CostructuredArrow.epi_iff_epi_left

added theorem CategoryTheory.StructuredArrow.mono_iff_mono_right