Commit 2024-03-26 07:43 dda2b3f9

View on Github →

feat: limits in the category of elements (#11484)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Elements.lean

added theorem CategoryTheory.CategoryOfElements.CreatesLimitsAux.map_lift_mapCone

added theorem CategoryTheory.CategoryOfElements.CreatesLimitsAux.map_π_liftedConeElement

added theorem CategoryTheory.CategoryOfElements.CreatesLimitsAux.π_liftedConeElement'