ColimitsCardinalClosure

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

Statistics

Metric	Count
Definitions colimitsCardinalClosure	1
Theorems colimitsCardinalClosure_le, instEssentiallySmallColimitsCardinalClosureOfLocallySmall, instIsClosedUnderColimitsOfShapeColimitsCardinalClosureCategoryFamily, instIsClosedUnderIsomorphismsColimitsCardinalClosure, isClosedUnderColimitsOfShape_colimitsCardinalClosure, isStableUnderRetracts_colimitsCardinalClosure, le_colimitsCardinalClosure	7
Total	8

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
colimitsCardinalClosure 📖	CompOp	12 math math: colimitsCardinalClosure_le_isCardinalPresentable, instIsClosedUnderColimitsOfShapeColimitsCardinalClosureCategoryFamily, instIsClosedUnderIsomorphismsColimitsCardinalClosure, instEssentiallySmallColimitsCardinalClosureOfLocallySmall, isStableUnderRetracts_colimitsCardinalClosure, IsStrongGenerator.isDense_colimitsCardinalClosure_ι, CategoryTheory.IsStrongGenerator.colimitsCardinalClosure_eq_isCardinalPresentable, isFiltered_costructuredArrow_colimitsCardinalClosure_ι, isClosedUnderColimitsOfShape_colimitsCardinalClosure, isCardinalFiltered_costructuredArrow_colimitsCardinalClosure_ι, colimitsCardinalClosure_le, le_colimitsCardinalClosure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
colimitsCardinalClosure_le 📖	mathematical	IsClosedUnderColimitsOfShape CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le	colimitsCardinalClosure	—	CategoryTheory.SmallCategoryCardinalLT.hasCardinalLT colimitsClosure_le
instEssentiallySmallColimitsCardinalClosureOfLocallySmall 📖	mathematical	—	EssentiallySmall colimitsCardinalClosure	—	instEssentiallySmallColimitsClosureOfSmallOfLocallySmall UnivLE.small UnivLE.self small_subtype CategoryTheory.locallySmall_of_univLE
instIsClosedUnderColimitsOfShapeColimitsCardinalClosureCategoryFamily 📖	mathematical	—	IsClosedUnderColimitsOfShape colimitsCardinalClosure CategoryTheory.SmallCategoryCardinalLT.categoryFamily CategoryTheory.SmallCategoryOfSet.instSmallCategoryElemObj Ordinal.ToType Cardinal.ord CategoryTheory.SmallCategoryOfSet HasCardinalLT CategoryTheory.Arrow Set.Elem CategoryTheory.SmallCategoryOfSet.obj	—	instIsClosedUnderColimitsOfShapeColimitsClosure
instIsClosedUnderIsomorphismsColimitsCardinalClosure 📖	mathematical	—	IsClosedUnderIsomorphisms colimitsCardinalClosure	—	instIsClosedUnderIsomorphismsColimitsClosure
isClosedUnderColimitsOfShape_colimitsCardinalClosure 📖	mathematical	HasCardinalLT CategoryTheory.Arrow	IsClosedUnderColimitsOfShape colimitsCardinalClosure	—	CategoryTheory.SmallCategoryCardinalLT.exists_equivalence isClosedUnderColimitsOfShape_iff_of_equivalence instIsClosedUnderColimitsOfShapeColimitsCardinalClosureCategoryFamily
isStableUnderRetracts_colimitsCardinalClosure 📖	mathematical	—	IsStableUnderRetracts colimitsCardinalClosure	—	isClosedUnderColimitsOfShape_colimitsCardinalClosure HasCardinalLT.of_le CategoryTheory.Arrow.finite Cardinal.IsRegular.aleph0_le Fact.out instIsStableUnderRetractsOfIsClosedUnderColimitsOfShapeWalkingParallelPair
le_colimitsCardinalClosure 📖	mathematical	—	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le colimitsCardinalClosure	—	le_colimitsClosure

---

← Back to Index