Limits

📁 Source: Mathlib/Condensed/Limits.lean

Statistics

Metric	Count
Definitions	0
Theorems instHasColimitsCondensedMod, instHasColimitsOfShapeCondensedOfHasWeakSheafifyCompHausCoherentTopology, instHasFiniteColimitsCondensedOfHasWeakSheafifyCompHausCoherentTopology, instHasFiniteLimitsCondensed, instHasLimitsCondensedMod, instHasLimitsCondensedSet, instHasLimitsOfShapeCondensed, instHasLimitsOfSizeCondensedMod, instHasLimitsOfSizeCondensedSet	9
Total	9

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasColimitsCondensedMod 📖	mathematical	—	CategoryTheory.Limits.HasColimits CondensedMod instCategoryCondensed ModuleCat ModuleCat.moduleCategory	—	—
instHasColimitsOfShapeCondensedOfHasWeakSheafifyCompHausCoherentTopology 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfShape Condensed instCategoryCondensed	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHaus.instHasExplicitFiniteCoproductsTrue CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHaus.instHasExplicitPullbacksTrue CompHaus.instPreregular
instHasFiniteColimitsCondensedOfHasWeakSheafifyCompHausCoherentTopology 📖	mathematical	—	CategoryTheory.Limits.HasFiniteColimits Condensed instCategoryCondensed	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHaus.instHasExplicitFiniteCoproductsTrue CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHaus.instHasExplicitPullbacksTrue CompHaus.instPreregular
instHasFiniteLimitsCondensed 📖	mathematical	—	CategoryTheory.Limits.HasFiniteLimits Condensed instCategoryCondensed	—	—
instHasLimitsCondensedMod 📖	mathematical	—	CategoryTheory.Limits.HasLimits CondensedMod instCategoryCondensed ModuleCat ModuleCat.moduleCategory	—	—
instHasLimitsCondensedSet 📖	mathematical	—	CategoryTheory.Limits.HasLimits CondensedSet instCategoryCondensed CategoryTheory.types	—	CategoryTheory.Sheaf.hasLimitsOfSize CategoryTheory.Limits.Types.hasLimitsOfSize UnivLE.self
instHasLimitsOfShapeCondensed 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfShape Condensed instCategoryCondensed	—	—
instHasLimitsOfSizeCondensedMod 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfSize CondensedMod instCategoryCondensed ModuleCat ModuleCat.moduleCategory	—	CategoryTheory.Limits.hasLimitsOfSizeShrink instHasLimitsCondensedMod
instHasLimitsOfSizeCondensedSet 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfSize CondensedSet instCategoryCondensed CategoryTheory.types	—	CategoryTheory.Limits.hasLimitsOfSizeShrink instHasLimitsCondensedSet

---

← Back to Index