Commit 2024-03-21 10:04 bba4917d

View on Github →

feat: add API for extension of cones (#11560)

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Cones.lean

added def CategoryTheory.Limits.Cocones.extend

added def CategoryTheory.Limits.Cocones.extendComp

added def CategoryTheory.Limits.Cocones.extendId

added def CategoryTheory.Limits.Cocones.extendIso

added def CategoryTheory.Limits.Cones.extend

added def CategoryTheory.Limits.Cones.extendComp

added def CategoryTheory.Limits.Cones.extendId

added def CategoryTheory.Limits.Cones.extendIso

Modified Mathlib/CategoryTheory/Limits/IsLimit.lean

added def CategoryTheory.Limits.IsColimit.extendIso

added def CategoryTheory.Limits.IsColimit.extendIsoEquiv

added def CategoryTheory.Limits.IsColimit.ofExtendIso

added def CategoryTheory.Limits.IsLimit.extendIso

added def CategoryTheory.Limits.IsLimit.extendIsoEquiv

added def CategoryTheory.Limits.IsLimit.ofExtendIso