Limits

📁 Source: Mathlib/Condensed/Light/Limits.lean

Statistics

Metric	Count
Definitions	0
Theorems instHasFiniteLimitsLightCondMod, instHasFiniteLimitsLightCondSet, instHasLimitsOfSizeLightCondMod, instHasLimitsOfSizeLightCondMod_1, instHasLimitsOfSizeLightCondSet	5
Total	5

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasFiniteLimitsLightCondMod 📖	mathematical	—	CategoryTheory.Limits.HasFiniteLimits LightCondMod instCategoryLightCondensed ModuleCat ModuleCat.moduleCategory	—	CategoryTheory.Limits.hasFiniteLimits_of_hasLimitsOfSize instHasLimitsOfSizeLightCondMod_1
instHasFiniteLimitsLightCondSet 📖	mathematical	—	CategoryTheory.Limits.HasFiniteLimits LightCondSet instCategoryLightCondensed CategoryTheory.types	—	CategoryTheory.Limits.hasFiniteLimits_of_hasLimitsOfSize instHasLimitsOfSizeLightCondSet
instHasLimitsOfSizeLightCondMod 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfSize LightCondMod instCategoryLightCondensed ModuleCat ModuleCat.moduleCategory	—	CategoryTheory.Sheaf.hasLimitsOfSize ModuleCat.hasLimits'
instHasLimitsOfSizeLightCondMod_1 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfSize LightCondMod instCategoryLightCondensed ModuleCat ModuleCat.moduleCategory	—	CategoryTheory.Sheaf.hasLimitsOfSize ModuleCat.instHasLimitsOfSize
instHasLimitsOfSizeLightCondSet 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfSize LightCondSet instCategoryLightCondensed CategoryTheory.types	—	CategoryTheory.Sheaf.hasLimitsOfSize CategoryTheory.Limits.Types.hasLimitsOfSize UnivLE.self

---

← Back to Index