Ulift

📁 Source: Mathlib/CategoryTheory/Limits/Preserves/Ulift.lean

Statistics

Metric	Count
Definitions instCreatesColimitsOfSizeUliftFunctor, instCreatesLimitsOfSizeUliftFunctor, sectionsEquiv	3
Theorems instPreservesColimitsOfSizeUliftFunctor, instPreservesLimitsOfSizeUliftFunctor	2
Total	5

CategoryTheory.Limits.Types

Definitions

Name	Category	Theorems
instCreatesColimitsOfSizeUliftFunctor 📖	CompOp	—
instCreatesLimitsOfSizeUliftFunctor 📖	CompOp	—
sectionsEquiv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instPreservesColimitsOfSizeUliftFunctor 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.types CategoryTheory.uliftFunctor	—	isColimit_iff_coconeTypesIsColimit CategoryTheory.Functor.CoconeTypes.IsColimit.of_equiv CategoryTheory.Functor.CoconeTypes.IsColimit.precompose
instPreservesLimitsOfSizeUliftFunctor 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfSize CategoryTheory.types CategoryTheory.uliftFunctor	—	isLimit_iff ULift.ext ULift.ext_iff

---

← Back to Index