Finite

📁 Source: Mathlib/CategoryTheory/Limits/Preserves/Creates/Finite.lean

Statistics

Metric	Count
Definitions createsFiniteColimits, createsFiniteColimits, createsFiniteColimits, CreatesFiniteColimits, createsFiniteColimits, CreatesFiniteCoproducts, creates, CreatesFiniteLimits, createsFiniteLimits, CreatesFiniteProducts, creates, createsFiniteLimits, createsFiniteLimits, createsFiniteLimits, compCreatesFiniteColimits, compCreatesFiniteCoproducts, compCreatesFiniteLimits, compCreatesFiniteProducts, createsColimitsOfShapeOfCreatesFiniteColimits, createsColimitsOfShapeOfCreatesFiniteProducts, createsFiniteColimitsOfCreatesFiniteColimitsOfSize, createsFiniteColimitsOfNatIso, createsFiniteCoproductsOfNatIso, createsFiniteLimitsOfCreatesFiniteLimitsOfSize, createsFiniteLimitsOfNatIso, createsFiniteProductsOfNatIso, createsLimitsOfShapeOfCreatesFiniteLimits, createsLimitsOfShapeOfCreatesFiniteProducts, instCreatesFiniteCoproductsOfCreatesFiniteColimits, instCreatesFiniteProductsOfCreatesFiniteLimits	30
Theorems hasFiniteColimits_of_hasColimits_of_createsFiniteColimits, hasFiniteLimits_of_hasLimitsLimits_of_createsFiniteLimits, preservesFiniteColimits_of_createsFiniteColimits_and_hasFiniteColimits, preservesFiniteLimits_of_createsFiniteLimits_and_hasFiniteLimits	4
Total	34

CategoryTheory.Limits

Definitions

Name	Category	Theorems
CreatesFiniteColimits 📖	CompData	—
CreatesFiniteCoproducts 📖	CompData	—
CreatesFiniteLimits 📖	CompData	—
CreatesFiniteProducts 📖	CompData	—
compCreatesFiniteColimits 📖	CompOp	—
compCreatesFiniteCoproducts 📖	CompOp	—
compCreatesFiniteLimits 📖	CompOp	—
compCreatesFiniteProducts 📖	CompOp	—
createsColimitsOfShapeOfCreatesFiniteColimits 📖	CompOp	—
createsColimitsOfShapeOfCreatesFiniteProducts 📖	CompOp	—
createsFiniteColimitsOfCreatesFiniteColimitsOfSize 📖	CompOp	—
createsFiniteColimitsOfNatIso 📖	CompOp	—
createsFiniteCoproductsOfNatIso 📖	CompOp	—
createsFiniteLimitsOfCreatesFiniteLimitsOfSize 📖	CompOp	—
createsFiniteLimitsOfNatIso 📖	CompOp	—
createsFiniteProductsOfNatIso 📖	CompOp	—
createsLimitsOfShapeOfCreatesFiniteLimits 📖	CompOp	—
createsLimitsOfShapeOfCreatesFiniteProducts 📖	CompOp	—
instCreatesFiniteCoproductsOfCreatesFiniteColimits 📖	CompOp	—
instCreatesFiniteProductsOfCreatesFiniteLimits 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasFiniteColimits_of_hasColimits_of_createsFiniteColimits 📖	mathematical	—	HasFiniteColimits	—	CategoryTheory.hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape hasColimitsOfShape_of_hasFiniteColimits
hasFiniteLimits_of_hasLimitsLimits_of_createsFiniteLimits 📖	mathematical	—	HasFiniteLimits	—	CategoryTheory.hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape hasLimitsOfShape_of_hasFiniteLimits
preservesFiniteColimits_of_createsFiniteColimits_and_hasFiniteColimits 📖	mathematical	—	PreservesFiniteColimits	—	CategoryTheory.preservesColimitOfShape_of_createsColimitsOfShape_and_hasColimitsOfShape hasColimitsOfShape_of_hasFiniteColimits
preservesFiniteLimits_of_createsFiniteLimits_and_hasFiniteLimits 📖	mathematical	—	PreservesFiniteLimits	—	CategoryTheory.preservesLimitOfShape_of_createsLimitsOfShape_and_hasLimitsOfShape hasLimitsOfShape_of_hasFiniteLimits

CategoryTheory.Limits.CreatesColimits

Definitions

Name	Category	Theorems
createsFiniteColimits 📖	CompOp	—

CategoryTheory.Limits.CreatesColimitsOfSize

Definitions

Name	Category	Theorems
createsFiniteColimits 📖	CompOp	—

CategoryTheory.Limits.CreatesColimitsOfSize0

Definitions

Name	Category	Theorems
createsFiniteColimits 📖	CompOp	—

CategoryTheory.Limits.CreatesFiniteColimits

Definitions

Name	Category	Theorems
createsFiniteColimits 📖	CompOp	—

CategoryTheory.Limits.CreatesFiniteCoproducts

Definitions

Name	Category	Theorems
creates 📖	CompOp	—

CategoryTheory.Limits.CreatesFiniteLimits

Definitions

Name	Category	Theorems
createsFiniteLimits 📖	CompOp	—

CategoryTheory.Limits.CreatesFiniteProducts

Definitions

Name	Category	Theorems
creates 📖	CompOp	—

CategoryTheory.Limits.CreatesLimits

Definitions

Name	Category	Theorems
createsFiniteLimits 📖	CompOp	—

CategoryTheory.Limits.CreatesLimitsOfSize

Definitions

Name	Category	Theorems
createsFiniteLimits 📖	CompOp	—

CategoryTheory.Limits.CreatesLimitsOfSize0

Definitions

Name	Category	Theorems
createsFiniteLimits 📖	CompOp	—

---

← Back to Index