Preserves

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

Statistics

Metric	Count
Definitions	0
Theorems preservesCoLimit_curriedTensor, preservesColimit_of_braided_and_preservesColimit_tensor_left, preservesColimit_of_braided_and_preservesColimit_tensor_right, preservesLimit_curriedTensor, preservesLimit_of_braided_and_preservesLimit_tensor_left, preservesLimit_of_braided_and_preservesLimit_tensor_right	6
Total	6

CategoryTheory.MonoidalCategory.Limits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preservesCoLimit_curriedTensor 📖	mathematical	CategoryTheory.Limits.PreservesColimit CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.curriedTensor	—	CategoryTheory.Limits.preservesColimit_of_evaluation
preservesColimit_of_braided_and_preservesColimit_tensor_left 📖	mathematical	—	CategoryTheory.Limits.PreservesColimit CategoryTheory.MonoidalCategory.tensorRight	—	CategoryTheory.Limits.preservesColimit_of_natIso
preservesColimit_of_braided_and_preservesColimit_tensor_right 📖	mathematical	—	CategoryTheory.Limits.PreservesColimit CategoryTheory.MonoidalCategory.tensorLeft	—	CategoryTheory.Limits.preservesColimit_of_natIso
preservesLimit_curriedTensor 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.curriedTensor	—	CategoryTheory.Limits.preservesLimit_of_evaluation
preservesLimit_of_braided_and_preservesLimit_tensor_left 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit CategoryTheory.MonoidalCategory.tensorRight	—	CategoryTheory.Limits.preservesLimit_of_natIso
preservesLimit_of_braided_and_preservesLimit_tensor_right 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit CategoryTheory.MonoidalCategory.tensorLeft	—	CategoryTheory.Limits.preservesLimit_of_natIso

---

← Back to Index