Skeleton

📁 Source: Mathlib/CategoryTheory/Limits/Skeleton.lean

Statistics

Metric	Count
Definitions	0
Theorems hasColimitsOfShape_skeleton, hasColimitsOfShape_thinSkeleton, hasColimitsOfSize_skeleton, hasColimitsOfSize_thinSkeleton, hasLimitsOfShape_skeleton, hasLimitsOfShape_thinSkeleton, hasLimitsOfSize_skeleton, hasLimitsOfSize_thinSkeleton	8
Total	8

CategoryTheory.Limits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasColimitsOfShape_skeleton 📖	mathematical	—	HasColimitsOfShape CategoryTheory.Skeleton CategoryTheory.instCategorySkeleton	—	CategoryTheory.hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape CategoryTheory.fromSkeleton.isEquivalence
hasColimitsOfShape_thinSkeleton 📖	mathematical	Quiver.IsThin CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	HasColimitsOfShape CategoryTheory.ThinSkeleton Preorder.smallCategory CategoryTheory.ThinSkeleton.preorder	—	CategoryTheory.hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape CategoryTheory.ThinSkeleton.fromThinSkeleton_isEquivalence
hasColimitsOfSize_skeleton 📖	mathematical	—	HasColimitsOfSize CategoryTheory.Skeleton CategoryTheory.instCategorySkeleton	—	CategoryTheory.hasColimits_of_hasColimits_createsColimits CategoryTheory.fromSkeleton.isEquivalence
hasColimitsOfSize_thinSkeleton 📖	mathematical	Quiver.IsThin CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	HasColimitsOfSize CategoryTheory.ThinSkeleton Preorder.smallCategory CategoryTheory.ThinSkeleton.preorder	—	CategoryTheory.hasColimits_of_hasColimits_createsColimits CategoryTheory.ThinSkeleton.fromThinSkeleton_isEquivalence
hasLimitsOfShape_skeleton 📖	mathematical	—	HasLimitsOfShape CategoryTheory.Skeleton CategoryTheory.instCategorySkeleton	—	CategoryTheory.hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape CategoryTheory.fromSkeleton.isEquivalence
hasLimitsOfShape_thinSkeleton 📖	mathematical	Quiver.IsThin CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	HasLimitsOfShape CategoryTheory.ThinSkeleton Preorder.smallCategory CategoryTheory.ThinSkeleton.preorder	—	CategoryTheory.hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape CategoryTheory.ThinSkeleton.fromThinSkeleton_isEquivalence
hasLimitsOfSize_skeleton 📖	mathematical	—	HasLimitsOfSize CategoryTheory.Skeleton CategoryTheory.instCategorySkeleton	—	CategoryTheory.hasLimits_of_hasLimits_createsLimits CategoryTheory.fromSkeleton.isEquivalence
hasLimitsOfSize_thinSkeleton 📖	mathematical	Quiver.IsThin CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	HasLimitsOfSize CategoryTheory.ThinSkeleton Preorder.smallCategory CategoryTheory.ThinSkeleton.preorder	—	CategoryTheory.hasLimits_of_hasLimits_createsLimits CategoryTheory.ThinSkeleton.fromThinSkeleton_isEquivalence

---

← Back to Index