Documentation Verification Report

ColimitsClosure

📁 Source: Mathlib/CategoryTheory/ObjectProperty/ColimitsClosure.lean

Statistics

Metric	Count
Definitions `colimitsClosure`	1
Theorems `colimitsClosure_eq_unop_limitsClosure`, `colimitsClosure_isoClosure`, `colimitsClosure_le`, `colimitsClosure_monotone`, `instEssentiallySmallColimitsClosureOfSmallOfLocallySmall`, `instIsClosedUnderColimitsOfShapeColimitsClosure`, `instIsClosedUnderIsomorphismsColimitsClosure`, `le_colimitsClosure`	8
Total	9

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
`colimitsClosure` 📖	CompData	8 math math: `instIsClosedUnderColimitsOfShapeColimitsClosure`, `instIsClosedUnderIsomorphismsColimitsClosure`, `colimitsClosure_isoClosure`, `instEssentiallySmallColimitsClosureOfSmallOfLocallySmall`, `le_colimitsClosure`, `colimitsClosure_eq_unop_limitsClosure`, `colimitsClosure_le`, `colimitsClosure_monotone`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`colimitsClosure_eq_unop_limitsClosure` 📖	mathematical	—	`colimitsClosure` `unop` `CategoryTheory.Category.toCategoryStruct` `limitsClosure` `Opposite` `CategoryTheory.Category.opposite` `op`	—	`le_antisymm` `colimitsClosure_le` `instIsClosedUnderIsomorphismsUnopOfOpposite` `instIsClosedUnderIsomorphismsLimitsClosure` `instIsClosedUnderColimitsOfShapeUnopOfIsClosedUnderLimitsOfShapeOpposite` `instIsClosedUnderLimitsOfShapeLimitsClosure` `op_monotone_iff` `op_unop` `le_limitsClosure` `limitsClosure_le` `instIsClosedUnderIsomorphismsOppositeOp` `instIsClosedUnderIsomorphismsColimitsClosure` `instIsClosedUnderLimitsOfShapeOppositeOpOfIsClosedUnderColimitsOfShape` `instIsClosedUnderColimitsOfShapeColimitsClosure` `le_colimitsClosure`
`colimitsClosure_isoClosure` 📖	mathematical	—	`colimitsClosure` `isoClosure`	—	`le_antisymm` `colimitsClosure_le` `instIsClosedUnderIsomorphismsColimitsClosure` `instIsClosedUnderColimitsOfShapeColimitsClosure` `isoClosure_le_iff` `le_colimitsClosure` `colimitsClosure_monotone` `le_isoClosure`
`colimitsClosure_le` 📖	mathematical	`IsClosedUnderColimitsOfShape` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.hasLe` `Prop.le`	`colimitsClosure`	—	`prop_of_iso` `prop_of_isColimit`
`colimitsClosure_monotone` 📖	mathematical	`CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.hasLe` `Prop.le`	`colimitsClosure`	—	`colimitsClosure_le` `instIsClosedUnderIsomorphismsColimitsClosure` `instIsClosedUnderColimitsOfShapeColimitsClosure` `LE.le.trans` `le_colimitsClosure`
`instEssentiallySmallColimitsClosureOfSmallOfLocallySmall` 📖	mathematical	`Small` `CategoryTheory.LocallySmall`	`EssentiallySmall` `colimitsClosure`	—	`colimitsClosure_eq_unop_limitsClosure` `Opposite.small` `instEssentiallySmallUnopOfOpposite` `instEssentiallySmallLimitsClosureOfSmallOfLocallySmall` `instEssentiallySmallOppositeOp` `CategoryTheory.instLocallySmallOpposite`
`instIsClosedUnderColimitsOfShapeColimitsClosure` 📖	mathematical	—	`IsClosedUnderColimitsOfShape` `colimitsClosure`	—	`ColimitOfShape.prop_diag_obj`
`instIsClosedUnderIsomorphismsColimitsClosure` 📖	mathematical	—	`IsClosedUnderIsomorphisms` `colimitsClosure`	—	—
`le_colimitsClosure` 📖	mathematical	—	`CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.hasLe` `Prop.le` `colimitsClosure`	—	—

---

← Back to Index