HasConicalLimits

📁 Source: Mathlib/CategoryTheory/Enriched/Limits/HasConicalLimits.lean

Statistics

Metric	Count
Definitions HasConicalLimit, HasConicalLimits, HasConicalLimitsOfShape, HasConicalLimitsOfSize	4
Theorems of_equiv, of_equiv_comp, of_iso, preservesLimit_eCoyoneda, toHasLimit, hasConicalLimit, hasLimitsOfShape, of_equiv, hasConicalLimitsOfShape, hasLimitsOfSize	10
Total	14

CategoryTheory.Enriched

Definitions

Name	Category	Theorems
HasConicalLimit 📖	CompData	4 math math: HasConicalLimit.of_iso, HasConicalLimitsOfShape.hasConicalLimit, HasConicalLimit.of_equiv, HasConicalLimit.of_equiv_comp
HasConicalLimits 📖	MathDef	—
HasConicalLimitsOfShape 📖	CompData	3 math math: HasConicalLimitsOfShape.of_equiv, HasConicalLimitsOfSize.hasConicalLimitsOfShape, HasConicalProducts.hasConicalLimitsOfShape
HasConicalLimitsOfSize 📖	CompData	—

CategoryTheory.Enriched.HasConicalLimit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_equiv 📖	mathematical	—	CategoryTheory.Enriched.HasConicalLimit CategoryTheory.Functor.comp	—	CategoryTheory.Functor.Initial.comp_hasLimit CategoryTheory.Functor.initial_of_isLeftAdjoint CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence toHasLimit CategoryTheory.Functor.Initial.comp_preservesLimit preservesLimit_eCoyoneda
of_equiv_comp 📖	mathematical	—	CategoryTheory.Enriched.HasConicalLimit	—	of_iso of_equiv CategoryTheory.Functor.isEquivalence_inv
of_iso 📖	mathematical	—	CategoryTheory.Enriched.HasConicalLimit	—	CategoryTheory.Limits.hasLimit_of_iso toHasLimit CategoryTheory.Limits.preservesLimit_of_iso_diagram preservesLimit_eCoyoneda
preservesLimit_eCoyoneda 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit CategoryTheory.eCoyoneda	—	—
toHasLimit 📖	mathematical	—	CategoryTheory.Limits.HasLimit	—	—

CategoryTheory.Enriched.HasConicalLimitsOfShape

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasConicalLimit 📖	mathematical	—	CategoryTheory.Enriched.HasConicalLimit	—	—
hasLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfShape	—	CategoryTheory.Enriched.HasConicalLimit.toHasLimit hasConicalLimit
of_equiv 📖	mathematical	—	CategoryTheory.Enriched.HasConicalLimitsOfShape	—	CategoryTheory.Enriched.HasConicalLimit.of_equiv_comp hasConicalLimit

CategoryTheory.Enriched.HasConicalLimitsOfSize

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasConicalLimitsOfShape 📖	mathematical	—	CategoryTheory.Enriched.HasConicalLimitsOfShape	—	—
hasLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfSize	—	CategoryTheory.Enriched.HasConicalLimitsOfShape.hasLimitsOfShape hasConicalLimitsOfShape

---

← Back to Index