Commit 2023-03-07 10:18 5c5f9d7e

View on Github →

feat: port CategoryTheory.Limits.FullSubcategory (#2690)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/FullSubcategory.lean

added theorem CategoryTheory.Limits.ClosedUnderColimitsOfShape.colimit

added def CategoryTheory.Limits.ClosedUnderColimitsOfShape

added theorem CategoryTheory.Limits.ClosedUnderLimitsOfShape.limit

added def CategoryTheory.Limits.ClosedUnderLimitsOfShape

added def CategoryTheory.Limits.createsColimitFullSubcategoryInclusion'

added def CategoryTheory.Limits.createsColimitFullSubcategoryInclusion

added def CategoryTheory.Limits.createsColimitFullSubcategoryInclusionOfClosed

added def CategoryTheory.Limits.createsColimitsOfShapeFullSubcategoryInclusion

added def CategoryTheory.Limits.createsLimitFullSubcategoryInclusion'

added def CategoryTheory.Limits.createsLimitFullSubcategoryInclusion

added def CategoryTheory.Limits.createsLimitFullSubcategoryInclusionOfClosed

added def CategoryTheory.Limits.createsLimitsOfShapeFullSubcategoryInclusion

added theorem CategoryTheory.Limits.hasColimit_of_closed_under_colimits

added theorem CategoryTheory.Limits.hasColimitsOfShape_of_closed_under_colimits

added theorem CategoryTheory.Limits.hasLimit_of_closed_under_limits

added theorem CategoryTheory.Limits.hasLimitsOfShape_of_closed_under_limits