LimitsClosure

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

Statistics

Metric	Count
Definitions limitClosure, limitsClosure, strictLimitsClosureIter, strictLimitsClosureStep	4
Theorems instEssentiallySmallLimitsClosureOfSmallOfLocallySmall, instIsClosedUnderIsomorphismsLimitsClosure, instIsClosedUnderLimitsOfShapeLimitClosure, instIsClosedUnderLimitsOfShapeLimitsClosure, instSmallStrictLimitsClosureIterOfLocallySmallOfSmallElemIio, isEssentiallySmall_limitsClosure, isoClosure_strictLimitsClosureIter_eq_limitsClosure, le_limitsClosure, le_strictLimitsClosureIter, le_strictLimitsClosureStep, limitsClosure_bot, limitsClosure_eq_self, limitsClosure_isoClosure, limitsClosure_le, limitsClosure_monotone, limitsClosure_top, strictLimitsClosureIter_le_limitsClosure, strictLimitsClosureStep_monotone, strictLimitsClosureStep_strictLimitsClosureIter_eq_self	19
Total	23

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
limitClosure 📖	CompOp	1 math math: instIsClosedUnderLimitsOfShapeLimitClosure
limitsClosure 📖	CompData	14 math math: limitsClosure_top, le_limitsClosure, limitsClosure_le, isEssentiallySmall_limitsClosure, strictLimitsClosureIter_le_limitsClosure, limitsClosure_eq_self, isoClosure_strictLimitsClosureIter_eq_limitsClosure, limitsClosure_isoClosure, instEssentiallySmallLimitsClosureOfSmallOfLocallySmall, colimitsClosure_eq_unop_limitsClosure, instIsClosedUnderLimitsOfShapeLimitsClosure, instIsClosedUnderIsomorphismsLimitsClosure, limitsClosure_monotone, limitsClosure_bot
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	—	—
instIsClosedUnderLimitsOfShapeLimitClosure 📖	mathematical	—	IsClosedUnderLimitsOfShape limitClosure	—	instIsClosedUnderLimitsOfShapeLimitsClosure
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_bot 📖	mathematical	—	limitsClosure Bot.bot CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.instBotForall BooleanAlgebra.toBot Prop.instBooleanAlgebra	—	limitsClosure_eq_self instIsClosedUnderIsomorphismsBot instIsClosedUnderLimitsOfShapeBotOfNonempty
limitsClosure_eq_self 📖	mathematical	IsClosedUnderLimitsOfShape	limitsClosure	—	le_antisymm limitsClosure_le le_refl le_limitsClosure
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	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	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le limitsClosure	—	limitsClosure_le instIsClosedUnderIsomorphismsLimitsClosure instIsClosedUnderLimitsOfShapeLimitsClosure LE.le.trans le_limitsClosure
limitsClosure_top 📖	mathematical	—	limitsClosure Top.top CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.instTopForall BooleanAlgebra.toTop Prop.instBooleanAlgebra	—	limitsClosure_eq_self instIsClosedUnderIsomorphismsTop instIsClosedUnderLimitsOfShapeTop
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	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_ord 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