Basic

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

Statistics

Metric	Count
Definitions instLaxMonoidalFunctorLim	1
Theorems lim_ε_π, lim_ε_π_assoc, lim_μ_π, lim_μ_π_assoc	4
Total	5

CategoryTheory.Limits

Definitions

Name	Category	Theorems
instLaxMonoidalFunctorLim 📖	CompOp	6 math math: CategoryTheory.Mon.limit_mon_mul, lim_ε_π_assoc, lim_ε_π, lim_μ_π_assoc, CategoryTheory.Mon.limit_mon_one, lim_μ_π

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lim_ε_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category lim CategoryTheory.Monoidal.functorCategoryMonoidal CategoryTheory.Functor.LaxMonoidal.ε instLaxMonoidalFunctorLim limit.π hasLimitOfHasLimitsOfShape CategoryTheory.CategoryStruct.id	—	limit.lift_π
lim_ε_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category lim CategoryTheory.Monoidal.functorCategoryMonoidal CategoryTheory.Functor.LaxMonoidal.ε instLaxMonoidalFunctorLim limit.π hasLimitOfHasLimitsOfShape	—	hasLimitOfHasLimitsOfShape CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' lim_ε_π
lim_μ_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category lim CategoryTheory.Monoidal.functorCategoryMonoidal CategoryTheory.Functor.LaxMonoidal.μ instLaxMonoidalFunctorLim limit.π hasLimitOfHasLimitsOfShape CategoryTheory.MonoidalCategoryStruct.tensorHom limit	—	limit.lift_π hasLimitOfHasLimitsOfShape
lim_μ_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category lim CategoryTheory.Monoidal.functorCategoryMonoidal CategoryTheory.Functor.LaxMonoidal.μ instLaxMonoidalFunctorLim limit.π hasLimitOfHasLimitsOfShape CategoryTheory.MonoidalCategoryStruct.tensorHom limit	—	hasLimitOfHasLimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lim_μ_π

---

← Back to Index