Basic

Statistics

Metric	Count
Definitions	0
Theorems `hasFiniteLimits`, `hasLimits`, `instHasEqualizers`, `instHasPullbacks`	4
Total	4

Name	Kind	Assumes	Proves	Validates	Depends On
`hasFiniteLimits` 📖	mathematical	—	`CategoryTheory.Limits.HasFiniteLimits` `CategoryTheory.Over` `CategoryTheory.instCategoryOver`	—	`ConstructProducts.over_finiteProducts_of_finiteWidePullbacks` `CategoryTheory.Limits.hasEqualizers_of_hasPullbacks_and_binary_products` `CategoryTheory.Limits.hasLimitsOfShape_discrete` `Finite.of_fintype` `instHasPullbacks` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `CategoryTheory.Limits.hasFiniteLimits_of_hasEqualizers_and_finite_products`
`hasLimits` 📖	mathematical	`CategoryTheory.Limits.HasWidePullbacks`	`CategoryTheory.Limits.HasLimitsOfSize` `CategoryTheory.Over` `CategoryTheory.instCategoryOver`	—	`ConstructProducts.over_binaryProduct_of_pullback` `CategoryTheory.Limits.hasPullbacks_of_hasWidePullbacks` `CategoryTheory.Limits.hasEqualizers_of_hasPullbacks_and_binary_products` `instHasPullbacks` `ConstructProducts.over_products_of_widePullbacks` `CategoryTheory.Limits.has_limits_of_hasEqualizers_and_products`
`instHasEqualizers` 📖	mathematical	—	`CategoryTheory.Limits.HasEqualizers` `CategoryTheory.Over` `CategoryTheory.instCategoryOver`	—	`hasLimitsOfShape_of_isConnected` `CategoryTheory.parallel_pair_connected`
`instHasPullbacks` 📖	mathematical	—	`CategoryTheory.Limits.HasPullbacks` `CategoryTheory.Over` `CategoryTheory.instCategoryOver`	—	`hasLimitsOfShape_of_isConnected` `CategoryTheory.widePullbackShape_connected`

---