Documentation Verification Report

LimitsClosure

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

Statistics

Metric	Count
Definitions `limitsClosure`, `strictLimitsClosureIter`, `strictLimitsClosureStep`	3
Theorems `instEssentiallySmallLimitsClosureOfSmallOfLocallySmall`, `instIsClosedUnderIsomorphismsLimitsClosure`, `instIsClosedUnderLimitsOfShapeLimitsClosure`, `instSmallStrictLimitsClosureIterOfLocallySmallOfSmallElemIio`, `isEssentiallySmall_limitsClosure`, `isoClosure_strictLimitsClosureIter_eq_limitsClosure`, `le_limitsClosure`, `le_strictLimitsClosureIter`, `le_strictLimitsClosureStep`, `limitsClosure_isoClosure`, `limitsClosure_le`, `limitsClosure_monotone`, `strictLimitsClosureIter_le_limitsClosure`, `strictLimitsClosureStep_monotone`, `strictLimitsClosureStep_strictLimitsClosureIter_eq_self`	15
Total	18

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
`limitsClosure` 📖	CompData	11 math math: `le_limitsClosure`, `limitsClosure_le`, `isEssentiallySmall_limitsClosure`, `strictLimitsClosureIter_le_limitsClosure`, `isoClosure_strictLimitsClosureIter_eq_limitsClosure`, `limitsClosure_isoClosure`, `instEssentiallySmallLimitsClosureOfSmallOfLocallySmall`, `colimitsClosure_eq_unop_limitsClosure`, `instIsClosedUnderLimitsOfShapeLimitsClosure`, `instIsClosedUnderIsomorphismsLimitsClosure`, `limitsClosure_monotone`
`strictLimitsClosureIter` 📖	CompOp	5 math math: `strictLimitsClosureIter_le_limitsClosure`, `isoClosure_strictLimitsClosureIter_eq_limitsClosure`, `strictLimitsClosureStep_strictLimitsClosureIter_eq_self`, `instSmallStrictLimitsClosureIterOfLocallySmallOfSmallElemIio`, `le_strictLimitsClosureIter`
`strictLimitsClosureStep` 📖	CompOp	3 math math: `le_strictLimitsClosureStep`, `strictLimitsClosureStep_monotone`, `strictLimitsClosureStep_strictLimitsClosureIter_eq_self`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instEssentiallySmallLimitsClosureOfSmallOfLocallySmall` 📖	mathematical	`Small` `CategoryTheory.LocallySmall`	`EssentiallySmall` `limitsClosure`	—	`HasCardinalLT.exists_regular_cardinal_forall` `isEssentiallySmall_limitsClosure`
`instIsClosedUnderIsomorphismsLimitsClosure` 📖	mathematical	—	`IsClosedUnderIsomorphisms` `limitsClosure`	—	—
`instIsClosedUnderLimitsOfShapeLimitsClosure` 📖	mathematical	—	`IsClosedUnderLimitsOfShape` `limitsClosure`	—	`LimitOfShape.prop_diag_obj`
`instSmallStrictLimitsClosureIterOfLocallySmallOfSmallElemIio` 📖	mathematical	`Small` `CategoryTheory.LocallySmall`	`Small` `strictLimitsClosureIter`	—	`small_of_injective` `lt_of_lt_of_le` `transfiniteIterate_bot` `IsMin.eq_bot` `Order.le_succ` `strictLimitsClosureIter.eq_1` `transfiniteIterate_succ` `strictLimitsClosureStep.eq_1` `instSmallMax` `instSmallISupOfSmall` `instSmallStrictLimitsOfShapeOfSmallOfLocallySmall` `transfiniteIterate_limit` `LT.lt.le`
`isEssentiallySmall_limitsClosure` 📖	mathematical	`HasCardinalLT` `Small` `CategoryTheory.LocallySmall`	`EssentiallySmall` `limitsClosure`	—	`EssentiallySmall.exists_small_le` `limitsClosure_isoClosure` `Ordinal.wellFoundedLT` `isoClosure_strictLimitsClosureIter_eq_limitsClosure` `instEssentiallySmallIsoClosure` `instEssentiallySmallOfSmall` `instSmallStrictLimitsClosureIterOfLocallySmallOfSmallElemIio` `Ordinal.small_Iio` `EssentiallySmall.of_le` `limitsClosure_monotone`
`isoClosure_strictLimitsClosureIter_eq_limitsClosure` 📖	mathematical	`HasCardinalLT`	`isoClosure` `strictLimitsClosureIter` `Ordinal` `Ordinal.instLinearOrder` `Ordinal.instSuccOrder` `Ordinal.wellFoundedLT` `Cardinal.ord` `limitsClosure`	—	`le_antisymm` `Ordinal.wellFoundedLT` `isoClosure_le_iff` `instIsClosedUnderIsomorphismsLimitsClosure` `strictLimitsClosureIter_le_limitsClosure` `strictLimitsClosureStep_strictLimitsClosureIter_eq_self` `limitsOfShape_isoClosure` `isoClosure_strictLimitsOfShape` `strictLimitsClosureStep.eq_1` `monotone_isoClosure` `LE.le.trans` `le_trans` `le_refl` `le_iSup` `le_sup_right` `limitsClosure_le` `instIsClosedUnderIsomorphismsIsoClosure` `le_strictLimitsClosureIter` `le_isoClosure`
`le_limitsClosure` 📖	mathematical	—	`CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.hasLe` `Prop.le` `limitsClosure`	—	—
`le_strictLimitsClosureIter` 📖	mathematical	—	`CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.hasLe` `Prop.le` `strictLimitsClosureIter`	—	`transfiniteIterate_bot` `monotone_transfiniteIterate` `le_strictLimitsClosureStep` `bot_le`
`le_strictLimitsClosureStep` 📖	mathematical	—	`CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.hasLe` `Prop.le` `strictLimitsClosureStep`	—	`le_sup_left`
`limitsClosure_isoClosure` 📖	mathematical	—	`limitsClosure` `isoClosure`	—	`le_antisymm` `limitsClosure_le` `instIsClosedUnderIsomorphismsLimitsClosure` `instIsClosedUnderLimitsOfShapeLimitsClosure` `isoClosure_le_iff` `le_limitsClosure` `limitsClosure_monotone` `le_isoClosure`
`limitsClosure_le` 📖	mathematical	`IsClosedUnderLimitsOfShape` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.hasLe` `Prop.le`	`limitsClosure`	—	`prop_of_iso` `prop_of_isLimit`
`limitsClosure_monotone` 📖	mathematical	`CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.hasLe` `Prop.le`	`limitsClosure`	—	`limitsClosure_le` `instIsClosedUnderIsomorphismsLimitsClosure` `instIsClosedUnderLimitsOfShapeLimitsClosure` `LE.le.trans` `le_limitsClosure`
`strictLimitsClosureIter_le_limitsClosure` 📖	mathematical	—	`CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.hasLe` `Prop.le` `strictLimitsClosureIter` `limitsClosure`	—	`transfiniteIterate_bot` `IsMin.eq_bot` `strictLimitsClosureIter.eq_1` `transfiniteIterate_succ` `strictLimitsClosureStep.eq_1` `sup_le_iff` `iSup_le_iff` `LE.le.trans` `strictLimitsOfShape_le_limitsOfShape` `limitsOfShape_monotone` `IsClosedUnderLimitsOfShape.limitsOfShape_le` `instIsClosedUnderLimitsOfShapeLimitsClosure` `transfiniteIterate_limit`
`strictLimitsClosureStep_monotone` 📖	mathematical	`CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.hasLe` `Prop.le`	`strictLimitsClosureStep`	—	`LE.le.trans` `le_sup_left` `strictLimitsOfShape_monotone` `le_iSup` `le_sup_right`
`strictLimitsClosureStep_strictLimitsClosureIter_eq_self` 📖	mathematical	`HasCardinalLT`	`strictLimitsClosureStep` `strictLimitsClosureIter` `Ordinal` `Ordinal.instLinearOrder` `Ordinal.instSuccOrder` `Ordinal.wellFoundedLT` `Cardinal.ord`	—	`Fact.out` `HasCardinalLT.small` `le_antisymm` `Ordinal.wellFoundedLT` `Ordinal.iSup_lt_ord` `Cardinal.IsRegular.cof_eq` `hasCardinalLT_iff_cardinal_mk_lt` `hasCardinalLT_iff_of_equiv` `Equiv.surjective` `le_ciSup` `Ordinal.bddAbove_range` `monotone_transfiniteIterate` `le_strictLimitsClosureStep` `Order.succ_le_iff` `Ordinal.instNoMaxOrder` `transfiniteIterate_succ` `transfiniteIterate_limit` `Cardinal.isSuccLimit_ord` `Cardinal.IsRegular.aleph0_le`

---

← Back to Index