Loogle!

Result

Found 101 declarations mentioning CategoryTheory.Limits.lim.

• CategoryTheory.Limits.lim 📋 Mathlib.CategoryTheory.Limits.HasLimits
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] : CategoryTheory.Functor (CategoryTheory.Functor J C) C
• CategoryTheory.Limits.instIsRightAdjointFunctorLim 📋 Mathlib.CategoryTheory.Limits.HasLimits
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] : CategoryTheory.Limits.lim.IsRightAdjoint
• CategoryTheory.Limits.constLimAdj 📋 Mathlib.CategoryTheory.Limits.HasLimits
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] : CategoryTheory.Functor.const J ⊣ CategoryTheory.Limits.lim
• CategoryTheory.Limits.lim_obj 📋 Mathlib.CategoryTheory.Limits.HasLimits
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] (F : CategoryTheory.Functor J C) : CategoryTheory.Limits.lim.obj F = CategoryTheory.Limits.limit F
• CategoryTheory.Limits.lim.π 📋 Mathlib.CategoryTheory.Limits.HasLimits
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] (j : J) : CategoryTheory.Limits.lim ⟶ (CategoryTheory.evaluation J C).obj j
• CategoryTheory.Limits.lim.π_app 📋 Mathlib.CategoryTheory.Limits.HasLimits
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] (j : J) (F : CategoryTheory.Functor J C) : (CategoryTheory.Limits.lim.π j).app F = CategoryTheory.Limits.limit.π F j
• CategoryTheory.Limits.limMap_eq 📋 Mathlib.CategoryTheory.Limits.HasLimits
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C} [CategoryTheory.Limits.HasLimitsOfShape J C] {G : CategoryTheory.Functor J C} (α : F ⟶ G) : CategoryTheory.Limits.limMap α = CategoryTheory.Limits.lim.map α
• CategoryTheory.Limits.lim_map 📋 Mathlib.CategoryTheory.Limits.HasLimits
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] {X✝ Y✝ : CategoryTheory.Functor J C} (α : X✝ ⟶ Y✝) : CategoryTheory.Limits.lim.map α = CategoryTheory.Limits.limMap α
• CategoryTheory.Limits.limit.id_pre 📋 Mathlib.CategoryTheory.Limits.HasLimits
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] (F : CategoryTheory.Functor J C) : CategoryTheory.Limits.limit.pre F (CategoryTheory.Functor.id J) = CategoryTheory.Limits.lim.map F.leftUnitor.inv
• CategoryTheory.Limits.limYoneda 📋 Mathlib.CategoryTheory.Limits.HasLimits
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] : CategoryTheory.Limits.lim.comp (CategoryTheory.yoneda.comp ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ (Type v) (Type (max v u₁))).obj CategoryTheory.uliftFunctor.{u₁, v})) ≅ CategoryTheory.cones J C
• CategoryTheory.Limits.limit.map_pre' 📋 Mathlib.CategoryTheory.Limits.HasLimits
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasLimitsOfShape K C] (F : CategoryTheory.Functor J C) {E₁ E₂ : CategoryTheory.Functor K J} (α : E₁ ⟶ E₂) : CategoryTheory.Limits.limit.pre F E₂ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.pre F E₁) (CategoryTheory.Limits.lim.map (CategoryTheory.Functor.whiskerRight α F))
• CategoryTheory.Limits.limit.map_pre 📋 Mathlib.CategoryTheory.Limits.HasLimits
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C} [CategoryTheory.Limits.HasLimitsOfShape J C] {G : CategoryTheory.Functor J C} (α : F ⟶ G) [CategoryTheory.Limits.HasLimitsOfShape K C] (E : CategoryTheory.Functor K J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.lim.map α) (CategoryTheory.Limits.limit.pre G E) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.pre F E) (CategoryTheory.Limits.lim.map (E.whiskerLeft α))
• CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompLim 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  (α : Type w₂) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProductsOfShape α C] : (CategoryTheory.piEquivalenceFunctorDiscrete α C).functor.comp CategoryTheory.Limits.lim ≅ CategoryTheory.Limits.Pi.functor α
• CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompLim_hom_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  (α : Type w₂) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProductsOfShape α C] (X : α → C) : (CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompLim α).hom.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.limit (CategoryTheory.Discrete.functor X))
• CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompLim_inv_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  (α : Type w₂) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProductsOfShape α C] (X : α → C) : (CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompLim α).inv.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.limit (CategoryTheory.Discrete.functor X))
• CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompLim_comp_functorπ 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProductsOfShape α C] (a : α) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompLim α).hom (CategoryTheory.Limits.Pi.functorπ a) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.piEquivalenceFunctorDiscrete α C).functor.whiskerLeft (CategoryTheory.Limits.lim.π { as := a })) (CategoryTheory.piEquivalenceFunctorDiscreteCompEvaluationIso C a).hom
• CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompLim_comp_functorπ_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProductsOfShape α C] (a : α) {Z : CategoryTheory.Functor (α → C) C} (h : CategoryTheory.Pi.eval (fun x => C) a ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompLim α).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.functorπ a) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.piEquivalenceFunctorDiscrete α C).functor.whiskerLeft (CategoryTheory.Limits.lim.π { as := a })) (CategoryTheory.CategoryStruct.comp (CategoryTheory.piEquivalenceFunctorDiscreteCompEvaluationIso C a).hom h)
• CategoryTheory.Limits.HasBiproductsOfShape.colimIsoLim 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBiproductsOfShape J C] : CategoryTheory.Limits.colim ≅ CategoryTheory.Limits.lim
• CategoryTheory.Limits.HasBiproductsOfShape.colimIsoLim_hom_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBiproductsOfShape J C] (X : CategoryTheory.Functor (CategoryTheory.Discrete J) C) : CategoryTheory.Limits.HasBiproductsOfShape.colimIsoLim.hom.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.isoColimit X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.desc (CategoryTheory.Limits.biproduct.ι fun j => X.obj { as := j })) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.lift (CategoryTheory.Limits.biproduct.π fun j => X.obj { as := j })) (CategoryTheory.Limits.Pi.isoLimit X).hom))
• CategoryTheory.Limits.HasBiproductsOfShape.colimIsoLim_inv_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBiproductsOfShape J C] (X : CategoryTheory.Functor (CategoryTheory.Discrete J) C) : CategoryTheory.Limits.HasBiproductsOfShape.colimIsoLim.inv.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.isoLimit X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.lift (CategoryTheory.Limits.Pi.π fun j => X.obj { as := j })) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.desc (CategoryTheory.Limits.Sigma.ι fun j => X.obj { as := j })) (CategoryTheory.Limits.Sigma.isoColimit X).hom))
• CategoryTheory.Limits.Types.limNatIsoSectionsFunctor 📋 Mathlib.CategoryTheory.Limits.Types.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] : CategoryTheory.Limits.lim ≅ CategoryTheory.Functor.sectionsFunctor J
• CategoryTheory.preservesLimitNatIso 📋 Mathlib.CategoryTheory.Limits.Preserves.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] [CategoryTheory.Limits.PreservesLimitsOfShape J G] [CategoryTheory.Limits.HasLimitsOfShape J D] [CategoryTheory.Limits.HasLimitsOfShape J C] : CategoryTheory.Limits.lim.comp G ≅ ((CategoryTheory.Functor.whiskeringRight J C D).obj G).comp CategoryTheory.Limits.lim
• CategoryTheory.preservesLimitNatIso_hom_app 📋 Mathlib.CategoryTheory.Limits.Preserves.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] [CategoryTheory.Limits.PreservesLimitsOfShape J G] [CategoryTheory.Limits.HasLimitsOfShape J D] [CategoryTheory.Limits.HasLimitsOfShape J C] (X : CategoryTheory.Functor J C) : (CategoryTheory.preservesLimitNatIso G).hom.app X = (CategoryTheory.preservesLimitIso G X).hom
• CategoryTheory.preservesLimitNatIso_inv_app 📋 Mathlib.CategoryTheory.Limits.Preserves.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] [CategoryTheory.Limits.PreservesLimitsOfShape J G] [CategoryTheory.Limits.HasLimitsOfShape J D] [CategoryTheory.Limits.HasLimitsOfShape J C] (X : CategoryTheory.Functor J C) : (CategoryTheory.preservesLimitNatIso G).inv.app X = (CategoryTheory.preservesLimitIso G X).inv
• CategoryTheory.Limits.limitIsoFlipCompLim 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasLimitsOfShape J C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) : CategoryTheory.Limits.limit F ≅ F.flip.comp CategoryTheory.Limits.lim
• CategoryTheory.Limits.limitFlipIsoCompLim 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasLimitsOfShape J C] (F : CategoryTheory.Functor K (CategoryTheory.Functor J C)) : CategoryTheory.Limits.limit F.flip ≅ F.comp CategoryTheory.Limits.lim
• CategoryTheory.Limits.limitIsoSwapCompLim 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasLimitsOfShape J C] (G : CategoryTheory.Functor J (CategoryTheory.Functor K C)) : CategoryTheory.Limits.limit G ≅ (CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp (CategoryTheory.Functor.uncurry.obj G))).comp CategoryTheory.Limits.lim
• CategoryTheory.Limits.limCompFlipIsoWhiskerLim 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasLimitsOfShape J C] : (CategoryTheory.flipFunctor K J C).comp CategoryTheory.Limits.lim ≅ (CategoryTheory.Functor.whiskeringRight K (CategoryTheory.Functor J C) C).obj CategoryTheory.Limits.lim
• CategoryTheory.Limits.limIsoFlipCompWhiskerLim 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasLimitsOfShape J C] : CategoryTheory.Limits.lim ≅ (CategoryTheory.flipFunctor J K C).comp ((CategoryTheory.Functor.whiskeringRight K (CategoryTheory.Functor J C) C).obj CategoryTheory.Limits.lim)
• CategoryTheory.Limits.limitIsoFlipCompLim_hom_app 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasLimitsOfShape J C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (X : K) : (CategoryTheory.Limits.limitIsoFlipCompLim F).hom.app X = (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation F X).hom
• CategoryTheory.Limits.limitIsoFlipCompLim_inv_app 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasLimitsOfShape J C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (X : K) : (CategoryTheory.Limits.limitIsoFlipCompLim F).inv.app X = (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation F X).inv
• CategoryTheory.Limits.limitFlipIsoCompLim_hom_app 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasLimitsOfShape J C] (F : CategoryTheory.Functor K (CategoryTheory.Functor J C)) (X : K) : (CategoryTheory.Limits.limitFlipIsoCompLim F).hom.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation F.flip X).hom (CategoryTheory.Limits.HasLimit.isoOfNatIso (CategoryTheory.flipCompEvaluation F X)).hom
• CategoryTheory.Limits.limitFlipIsoCompLim_inv_app 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasLimitsOfShape J C] (F : CategoryTheory.Functor K (CategoryTheory.Functor J C)) (X : K) : (CategoryTheory.Limits.limitFlipIsoCompLim F).inv.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.HasLimit.isoOfNatIso (CategoryTheory.flipCompEvaluation F X)).inv (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation F.flip X).inv
• CategoryTheory.Limits.limIsoFlipCompWhiskerLim_hom_app_app 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasLimitsOfShape J C] (X : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (X✝ : K) : (CategoryTheory.Limits.limIsoFlipCompWhiskerLim.hom.app X).app X✝ = (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation X X✝).hom
• CategoryTheory.Limits.limIsoFlipCompWhiskerLim_inv_app_app 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasLimitsOfShape J C] (X : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (X✝ : K) : (CategoryTheory.Limits.limIsoFlipCompWhiskerLim.inv.app X).app X✝ = (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation X X✝).inv
• CategoryTheory.Limits.limCompFlipIsoWhiskerLim_hom_app_app 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasLimitsOfShape J C] (X : CategoryTheory.Functor K (CategoryTheory.Functor J C)) (X✝ : K) : (CategoryTheory.Limits.limCompFlipIsoWhiskerLim.hom.app X).app X✝ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation X.flip X✝).hom (CategoryTheory.Limits.HasLimit.isoOfNatIso (CategoryTheory.flipCompEvaluation X X✝)).hom
• CategoryTheory.Limits.limCompFlipIsoWhiskerLim_inv_app_app 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasLimitsOfShape J C] (X : CategoryTheory.Functor K (CategoryTheory.Functor J C)) (X✝ : K) : (CategoryTheory.Limits.limCompFlipIsoWhiskerLim.inv.app X).app X✝ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.HasLimit.isoOfNatIso (CategoryTheory.flipCompEvaluation X X✝)).inv (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation X.flip X✝).inv
• CategoryTheory.Limits.limitIsoSwapCompLim_hom_app 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasLimitsOfShape J C] (G : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (X : K) : (CategoryTheory.Limits.limitIsoSwapCompLim G).hom.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation G X).hom (CategoryTheory.Limits.limMap (G.flipIsoCurrySwapUncurry.hom.app X))
• CategoryTheory.Limits.limitIsoSwapCompLim_inv_app 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasLimitsOfShape J C] (G : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (X : K) : (CategoryTheory.Limits.limitIsoSwapCompLim G).inv.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limMap (G.flipIsoCurrySwapUncurry.inv.app X)) (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation G X).inv
• CategoryTheory.Adjunction.lim_preservesLimits 📋 Mathlib.CategoryTheory.Adjunction.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] [CategoryTheory.Limits.HasLimitsOfShape J C] : CategoryTheory.Limits.PreservesLimits CategoryTheory.Limits.lim
• CategoryTheory.Functor.Initial.limIso 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.Limits.HasLimitsOfShape D E] [CategoryTheory.Limits.HasLimitsOfShape C E] : ((CategoryTheory.Functor.whiskeringLeft C D E).obj F).comp CategoryTheory.Limits.lim ≅ CategoryTheory.Limits.lim
• CategoryTheory.Limits.yonedaCompLimIsoCocones 📋 Mathlib.CategoryTheory.Limits.Types.Yoneda
  {J : Type v} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C) : CategoryTheory.yoneda.comp (((CategoryTheory.Functor.whiskeringLeft Jᵒᵖ Cᵒᵖ (Type v)).obj F.op).comp CategoryTheory.Limits.lim) ≅ F.cocones
• CategoryTheory.Limits.whiskeringLimYonedaIsoCones 📋 Mathlib.CategoryTheory.Limits.Types.Yoneda
  (J : Type v) [CategoryTheory.SmallCategory J] (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.Functor.whiskeringLeft J C (Type v)).comp (((CategoryTheory.Functor.whiskeringRight (CategoryTheory.Functor C (Type v)) (CategoryTheory.Functor J (Type v)) (Type v)).obj CategoryTheory.Limits.lim).comp ((CategoryTheory.Functor.whiskeringLeft Cᵒᵖ (CategoryTheory.Functor C (Type v)) (Type v)).obj CategoryTheory.coyoneda)) ≅ CategoryTheory.cones J C
• CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones 📋 Mathlib.CategoryTheory.Limits.Types.Yoneda
  (J : Type v) [CategoryTheory.SmallCategory J] (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.Functor.opHom J C).comp ((CategoryTheory.Functor.whiskeringLeft Jᵒᵖ Cᵒᵖ (Type v)).comp (((CategoryTheory.Functor.whiskeringRight (CategoryTheory.Functor Cᵒᵖ (Type v)) (CategoryTheory.Functor Jᵒᵖ (Type v)) (Type v)).obj CategoryTheory.Limits.lim).comp ((CategoryTheory.Functor.whiskeringLeft C (CategoryTheory.Functor Cᵒᵖ (Type v)) (Type v)).obj CategoryTheory.yoneda))) ≅ CategoryTheory.cocones J C
• CategoryTheory.Limits.whiskeringLimYonedaIsoCones_hom_app_app_hom_apply_app 📋 Mathlib.CategoryTheory.Limits.Types.Yoneda
  (J : Type v) [CategoryTheory.SmallCategory J] (C : Type u) [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor J C) (X✝ : Cᵒᵖ) (a : CategoryTheory.Limits.limit (X.comp (CategoryTheory.coyoneda.obj (Opposite.op (Opposite.unop X✝))))) (j : J) : ((CategoryTheory.ConcreteCategory.hom (((CategoryTheory.Limits.whiskeringLimYonedaIsoCones J C).hom.app X).app X✝)) a).app j = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π (X.comp (CategoryTheory.coyoneda.obj X✝)) j)) a
• CategoryTheory.Limits.whiskeringLimYonedaIsoCones_inv_app_app_hom_apply 📋 Mathlib.CategoryTheory.Limits.Types.Yoneda
  (J : Type v) [CategoryTheory.SmallCategory J] (C : Type u) [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor J C) (X✝ : Cᵒᵖ) (t : (CategoryTheory.Functor.const J).obj (Opposite.unop X✝) ⟶ X) : (CategoryTheory.ConcreteCategory.hom (((CategoryTheory.Limits.whiskeringLimYonedaIsoCones J C).inv.app X).app X✝)) t = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.lift (X.comp (CategoryTheory.coyoneda.obj X✝)) (CategoryTheory.Limits.Types.coneOfSection ⋯))) PUnit.unit
• CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones_hom_app_app_hom_apply_app 📋 Mathlib.CategoryTheory.Limits.Types.Yoneda
  (J : Type v) [CategoryTheory.SmallCategory J] (C : Type u) [CategoryTheory.Category.{v, u} C] (X : (CategoryTheory.Functor J C)ᵒᵖ) (X✝ : C) (a : CategoryTheory.Limits.limit ((Opposite.unop X).op.comp (CategoryTheory.yoneda.obj X✝))) (j : J) : ((CategoryTheory.ConcreteCategory.hom (((CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones J C).hom.app X).app X✝)) a).app j = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π ((Opposite.unop X).op.comp (CategoryTheory.yoneda.obj X✝)) (Opposite.op j))) a
• CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones_inv_app_app_hom_apply 📋 Mathlib.CategoryTheory.Limits.Types.Yoneda
  (J : Type v) [CategoryTheory.SmallCategory J] (C : Type u) [CategoryTheory.Category.{v, u} C] (X : (CategoryTheory.Functor J C)ᵒᵖ) (X✝ : C) (t : Opposite.unop X ⟶ (CategoryTheory.Functor.const J).obj X✝) : (CategoryTheory.ConcreteCategory.hom (((CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones J C).inv.app X).app X✝)) t = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.lift ((Opposite.unop X).op.comp (CategoryTheory.yoneda.obj X✝)) (CategoryTheory.Limits.Types.coneOfSection ⋯))) PUnit.unit
• CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimIso 📋 Mathlib.CategoryTheory.Limits.Constructions.Filtered
  (C : Type u) [CategoryTheory.Category.{v, u} C] (α : Type w) [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasLimitsOfShape (Finset (CategoryTheory.Discrete α))ᵒᵖ C] [CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete α) C] : (CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset C α).comp CategoryTheory.Limits.lim ≅ CategoryTheory.Limits.lim
• CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetEvaluationIso 📋 Mathlib.CategoryTheory.Limits.Constructions.Filtered
  (C : Type u) [CategoryTheory.Category.{v, u} C] (α : Type w) [CategoryTheory.Limits.HasFiniteProducts C] (I : Finset (CategoryTheory.Discrete α)) : (CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset C α).comp ((CategoryTheory.evaluation (Finset (CategoryTheory.Discrete α))ᵒᵖ C).obj (Opposite.op I)) ≅ ((CategoryTheory.Functor.whiskeringLeft (CategoryTheory.Discrete ↥I) (CategoryTheory.Discrete α) C).obj (CategoryTheory.Discrete.functor fun x => ↑x)).comp CategoryTheory.Limits.lim
• CategoryTheory.Functor.ranCompLimIso 📋 Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {H : Type u_3} [CategoryTheory.Category.{v_3, u_3} H] (L : CategoryTheory.Functor C D) [∀ (G : CategoryTheory.Functor C H), L.HasRightKanExtension G] [CategoryTheory.Limits.HasLimitsOfShape C H] [CategoryTheory.Limits.HasLimitsOfShape D H] : L.ran.comp CategoryTheory.Limits.lim ≅ CategoryTheory.Limits.lim
• CategoryTheory.Functor.ranCompLimIso_hom_app 📋 Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {H : Type u_3} [CategoryTheory.Category.{v_3, u_3} H] (L : CategoryTheory.Functor C D) [∀ (G : CategoryTheory.Functor C H), L.HasRightKanExtension G] [CategoryTheory.Limits.HasLimitsOfShape C H] [CategoryTheory.Limits.HasLimitsOfShape D H] (X : CategoryTheory.Functor C H) : L.ranCompLimIso.hom.app X = ((L.ran.obj X).limitIsoOfIsRightKanExtension (L.ranCounit.app X)).hom
• CategoryTheory.Functor.ranCompLimIso_inv_app 📋 Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {H : Type u_3} [CategoryTheory.Category.{v_3, u_3} H] (L : CategoryTheory.Functor C D) [∀ (G : CategoryTheory.Functor C H), L.HasRightKanExtension G] [CategoryTheory.Limits.HasLimitsOfShape C H] [CategoryTheory.Limits.HasLimitsOfShape D H] (X : CategoryTheory.Functor C H) : L.ranCompLimIso.inv.app X = ((L.ran.obj X).limitIsoOfIsRightKanExtension (L.ranCounit.app X)).inv
• CategoryTheory.instPreservesColimitsOfShapeFunctorLim 📋 Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] [CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.Limits.HasLimitsOfShape K C] [CategoryTheory.Limits.PreservesColimitsOfShape J CategoryTheory.Limits.lim] : CategoryTheory.Limits.PreservesColimitsOfShape J CategoryTheory.Limits.lim
• CategoryTheory.HasExactLimitsOfShape.mk 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
  {J : Type u'} [CategoryTheory.Category.{v', u'} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] (preservesFiniteColimits : CategoryTheory.Limits.PreservesFiniteColimits CategoryTheory.Limits.lim) : CategoryTheory.HasExactLimitsOfShape J C
• CategoryTheory.HasExactLimitsOfShape.preservesFiniteColimits 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
  {J : Type u'} {inst✝ : CategoryTheory.Category.{v', u'} J} {C : Type u} {inst✝¹ : CategoryTheory.Category.{v, u} C} {inst✝² : CategoryTheory.Limits.HasLimitsOfShape J C} [self : CategoryTheory.HasExactLimitsOfShape J C] : CategoryTheory.Limits.PreservesFiniteColimits CategoryTheory.Limits.lim
• CategoryTheory.hasExactLimitsOfShape_of_preservesEpi 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (J : Type u') [CategoryTheory.Category.{v', u'} J] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.lim.PreservesEpimorphisms] : CategoryTheory.HasExactLimitsOfShape J C
• CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits_conePoints 📋 Mathlib.CategoryTheory.Limits.Fubini
  {J : Type u_1} {K : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [CategoryTheory.Category.{v_3, u_3} C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [CategoryTheory.Limits.HasLimitsOfShape K C] : (CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits F).conePoints = F.comp CategoryTheory.Limits.lim
• CategoryTheory.Limits.coneOfHasLimitCurryCompLim 📋 Mathlib.CategoryTheory.Limits.Fubini
  {J : Type u_1} {K : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [CategoryTheory.Category.{v_3, u_3} C] (G : CategoryTheory.Functor (J × K) C) [CategoryTheory.Limits.HasLimitsOfShape K C] [CategoryTheory.Limits.HasLimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim)] : CategoryTheory.Limits.Cone G
• CategoryTheory.Limits.instHasLimitProd 📋 Mathlib.CategoryTheory.Limits.Fubini
  {J : Type u_1} {K : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [CategoryTheory.Category.{v_3, u_3} C] (G : CategoryTheory.Functor (J × K) C) [CategoryTheory.Limits.HasLimitsOfShape K C] [CategoryTheory.Limits.HasLimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim)] : CategoryTheory.Limits.HasLimit G
• CategoryTheory.Limits.isLimitConeOfHasLimitCurryCompLim 📋 Mathlib.CategoryTheory.Limits.Fubini
  {J : Type u_1} {K : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [CategoryTheory.Category.{v_3, u_3} C] (G : CategoryTheory.Functor (J × K) C) [CategoryTheory.Limits.HasLimitsOfShape K C] [CategoryTheory.Limits.HasLimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim)] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneOfHasLimitCurryCompLim G)
• CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim 📋 Mathlib.CategoryTheory.Limits.Fubini
  {J : Type u_1} {K : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [CategoryTheory.Category.{v_3, u_3} C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasLimitsOfShape K C] : CategoryTheory.Limits.limit (F.flip.comp CategoryTheory.Limits.lim) ≅ CategoryTheory.Limits.limit (F.comp CategoryTheory.Limits.lim)
• CategoryTheory.Limits.limitIsoLimitCurryCompLim 📋 Mathlib.CategoryTheory.Limits.Fubini
  {J : Type u_1} {K : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [CategoryTheory.Category.{v_3, u_3} C] (G : CategoryTheory.Functor (J × K) C) [CategoryTheory.Limits.HasLimitsOfShape K C] [CategoryTheory.Limits.HasLimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim)] : CategoryTheory.Limits.limit G ≅ CategoryTheory.Limits.limit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim)
• CategoryTheory.Limits.limitUncurryIsoLimitCompLim 📋 Mathlib.CategoryTheory.Limits.Fubini
  {J : Type u_1} {K : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [CategoryTheory.Category.{v_3, u_3} C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [CategoryTheory.Limits.HasLimitsOfShape K C] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.uncurry.obj F)] [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.Limits.lim)] : CategoryTheory.Limits.limit (CategoryTheory.Functor.uncurry.obj F) ≅ CategoryTheory.Limits.limit (F.comp CategoryTheory.Limits.lim)
• CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits_map_hom 📋 Mathlib.CategoryTheory.Limits.Fubini
  {J : Type u_1} {K : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [CategoryTheory.Category.{v_3, u_3} C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [CategoryTheory.Limits.HasLimitsOfShape K C] {j✝ j'✝ : J} (f : j✝ ⟶ j'✝) : ((CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits F).map f).hom = CategoryTheory.Limits.lim.map (F.map f)
• CategoryTheory.Limits.limitCurrySwapCompLimIsoLimitCurryCompLim 📋 Mathlib.CategoryTheory.Limits.Fubini
  {J : Type u_1} {K : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [CategoryTheory.Category.{v_3, u_3} C] (G : CategoryTheory.Functor (J × K) C) [CategoryTheory.Limits.HasLimitsOfShape K C] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasLimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim)] : CategoryTheory.Limits.limit ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp G)).comp CategoryTheory.Limits.lim) ≅ CategoryTheory.Limits.limit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim)
• CategoryTheory.Limits.limitUncurryIsoLimitCompLim_hom_π_π 📋 Mathlib.CategoryTheory.Limits.Fubini
  {J : Type u_1} {K : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [CategoryTheory.Category.{v_3, u_3} C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [CategoryTheory.Limits.HasLimitsOfShape K C] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.uncurry.obj F)] [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.Limits.lim)] {j : J} {k : K} : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitUncurryIsoLimitCompLim F).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.comp CategoryTheory.Limits.lim) j) (CategoryTheory.Limits.limit.π (F.obj j) k)) = CategoryTheory.Limits.limit.π (CategoryTheory.Functor.uncurry.obj F) (j, k)
• CategoryTheory.Limits.limitUncurryIsoLimitCompLim_inv_π 📋 Mathlib.CategoryTheory.Limits.Fubini
  {J : Type u_1} {K : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [CategoryTheory.Category.{v_3, u_3} C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [CategoryTheory.Limits.HasLimitsOfShape K C] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.uncurry.obj F)] [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.Limits.lim)] {j : J} {k : K} : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitUncurryIsoLimitCompLim F).inv (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.uncurry.obj F) (j, k)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.comp CategoryTheory.Limits.lim) j) (CategoryTheory.Limits.limit.π (F.obj j) k)
• CategoryTheory.Limits.limitUncurryIsoLimitCompLim_hom_π_π_assoc 📋 Mathlib.CategoryTheory.Limits.Fubini
  {J : Type u_1} {K : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [CategoryTheory.Category.{v_3, u_3} C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [CategoryTheory.Limits.HasLimitsOfShape K C] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.uncurry.obj F)] [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.Limits.lim)] {j : J} {k : K} {Z : C} (h : (F.obj j).obj k ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitUncurryIsoLimitCompLim F).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.comp CategoryTheory.Limits.lim) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.obj j) k) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.uncurry.obj F) (j, k)) h
• CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim_hom_π_π 📋 Mathlib.CategoryTheory.Limits.Fubini
  {J : Type u_1} {K : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [CategoryTheory.Category.{v_3, u_3} C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasLimitsOfShape K C] (j : J) (k : K) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim F).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.comp CategoryTheory.Limits.lim) j) (CategoryTheory.Limits.limit.π (F.obj j) k)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.flip.comp CategoryTheory.Limits.lim) k) (CategoryTheory.Limits.limit.π (F.flip.obj k) j)
• CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim_inv_π_π 📋 Mathlib.CategoryTheory.Limits.Fubini
  {J : Type u_1} {K : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [CategoryTheory.Category.{v_3, u_3} C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasLimitsOfShape K C] (k : K) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim F).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.flip.comp CategoryTheory.Limits.lim) k) (CategoryTheory.Limits.limit.π (F.flip.obj k) j)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.comp CategoryTheory.Limits.lim) j) (CategoryTheory.Limits.limit.π (F.obj j) k)
• CategoryTheory.Limits.limitIsoLimitCurryCompLim_inv_π 📋 Mathlib.CategoryTheory.Limits.Fubini
  {J : Type u_1} {K : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [CategoryTheory.Category.{v_3, u_3} C] (G : CategoryTheory.Functor (J × K) C) [CategoryTheory.Limits.HasLimitsOfShape K C] [CategoryTheory.Limits.HasLimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim)] {j : J} {k : K} : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitIsoLimitCurryCompLim G).inv (CategoryTheory.Limits.limit.π G (j, k)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim) j) (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj G).obj j) k)
• CategoryTheory.Limits.limitUncurryIsoLimitCompLim_inv_π_assoc 📋 Mathlib.CategoryTheory.Limits.Fubini
  {J : Type u_1} {K : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [CategoryTheory.Category.{v_3, u_3} C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [CategoryTheory.Limits.HasLimitsOfShape K C] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.uncurry.obj F)] [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.Limits.lim)] {j : J} {k : K} {Z : C} (h : (CategoryTheory.Functor.uncurry.obj F).obj (j, k) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitUncurryIsoLimitCompLim F).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.uncurry.obj F) (j, k)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.comp CategoryTheory.Limits.lim) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.obj j) k) h)
• CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim_hom_π_π_assoc 📋 Mathlib.CategoryTheory.Limits.Fubini
  {J : Type u_1} {K : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [CategoryTheory.Category.{v_3, u_3} C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasLimitsOfShape K C] (j : J) (k : K) {Z : C} (h : (F.obj j).obj k ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim F).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.comp CategoryTheory.Limits.lim) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.obj j) k) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.flip.comp CategoryTheory.Limits.lim) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.flip.obj k) j) h)
• CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim_inv_π_π_assoc 📋 Mathlib.CategoryTheory.Limits.Fubini
  {J : Type u_1} {K : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [CategoryTheory.Category.{v_3, u_3} C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasLimitsOfShape K C] (k : K) (j : J) {Z : C} (h : (F.flip.obj k).obj j ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim F).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.flip.comp CategoryTheory.Limits.lim) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.flip.obj k) j) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.comp CategoryTheory.Limits.lim) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.obj j) k) h)
• CategoryTheory.Limits.limitIsoLimitCurryCompLim_hom_π_π 📋 Mathlib.CategoryTheory.Limits.Fubini
  {J : Type u_1} {K : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [CategoryTheory.Category.{v_3, u_3} C] (G : CategoryTheory.Functor (J × K) C) [CategoryTheory.Limits.HasLimitsOfShape K C] [CategoryTheory.Limits.HasLimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim)] {j : J} {k : K} : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitIsoLimitCurryCompLim G).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim) j) (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj G).obj j) k)) = CategoryTheory.Limits.limit.π G (j, k)
• CategoryTheory.Limits.limitIsoLimitCurryCompLim_inv_π_assoc 📋 Mathlib.CategoryTheory.Limits.Fubini
  {J : Type u_1} {K : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [CategoryTheory.Category.{v_3, u_3} C] (G : CategoryTheory.Functor (J × K) C) [CategoryTheory.Limits.HasLimitsOfShape K C] [CategoryTheory.Limits.HasLimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim)] {j : J} {k : K} {Z : C} (h : G.obj (j, k) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitIsoLimitCurryCompLim G).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π G (j, k)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj G).obj j) k) h)
• CategoryTheory.Limits.limitIsoLimitCurryCompLim_hom_π_π_assoc 📋 Mathlib.CategoryTheory.Limits.Fubini
  {J : Type u_1} {K : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [CategoryTheory.Category.{v_3, u_3} C] (G : CategoryTheory.Functor (J × K) C) [CategoryTheory.Limits.HasLimitsOfShape K C] [CategoryTheory.Limits.HasLimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim)] {j : J} {k : K} {Z : C} (h : ((CategoryTheory.Functor.curry.obj G).obj j).obj k ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitIsoLimitCurryCompLim G).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj G).obj j) k) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π G (j, k)) h
• CategoryTheory.Limits.limitCurrySwapCompLimIsoLimitCurryCompLim_inv_π_π 📋 Mathlib.CategoryTheory.Limits.Fubini
  {J : Type u_1} {K : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [CategoryTheory.Category.{v_3, u_3} C] (G : CategoryTheory.Functor (J × K) C) [CategoryTheory.Limits.HasLimitsOfShape K C] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasLimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim)] {j : J} {k : K} : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitCurrySwapCompLimIsoLimitCurryCompLim G).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp G)).comp CategoryTheory.Limits.lim) k) (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp G)).obj k) j)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim) j) (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj G).obj j) k)
• CategoryTheory.Limits.limitCurrySwapCompLimIsoLimitCurryCompLim_hom_π_π 📋 Mathlib.CategoryTheory.Limits.Fubini
  {J : Type u_1} {K : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [CategoryTheory.Category.{v_3, u_3} C] (G : CategoryTheory.Functor (J × K) C) [CategoryTheory.Limits.HasLimitsOfShape K C] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasLimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim)] {j : J} {k : K} : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitCurrySwapCompLimIsoLimitCurryCompLim G).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim) j) (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj G).obj j) k)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp G)).comp CategoryTheory.Limits.lim) k) (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp G)).obj k) j)
• CategoryTheory.Limits.colimitLimitToLimitColimit 📋 Mathlib.CategoryTheory.Limits.ColimitLimit
  {J : Type u₁} {K : Type u₂} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.Category.{v₂, u₂} K] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor (J × K) C) [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape K C] : CategoryTheory.Limits.colimit ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp F)).comp CategoryTheory.Limits.lim) ⟶ CategoryTheory.Limits.limit ((CategoryTheory.Functor.curry.obj F).comp CategoryTheory.Limits.colim)
• CategoryTheory.Limits.ι_colimitLimitToLimitColimit_π 📋 Mathlib.CategoryTheory.Limits.ColimitLimit
  {J : Type u₁} {K : Type u₂} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.Category.{v₂, u₂} K] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor (J × K) C) [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape K C] (j : J) (k : K) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp F)).comp CategoryTheory.Limits.lim) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitLimitToLimitColimit F) (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj F).comp CategoryTheory.Limits.colim) j)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp F)).obj k) j) (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj F).obj j) k)
• CategoryTheory.Limits.ι_colimitLimitToLimitColimit_π_assoc 📋 Mathlib.CategoryTheory.Limits.ColimitLimit
  {J : Type u₁} {K : Type u₂} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.Category.{v₂, u₂} K] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor (J × K) C) [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape K C] (j : J) (k : K) {Z : C} (h : CategoryTheory.Limits.colim.obj ((CategoryTheory.Functor.curry.obj F).obj j) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp F)).comp CategoryTheory.Limits.lim) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitLimitToLimitColimit F) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj F).comp CategoryTheory.Limits.colim) j) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp F)).obj k) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj F).obj j) k) h)
• CategoryTheory.Limits.colimitLimitToLimitColimitCone_hom 📋 Mathlib.CategoryTheory.Limits.ColimitLimit
  {J : Type u₁} {K : Type u₂} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.Category.{v₂, u₂} K] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape K C] (G : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [CategoryTheory.Limits.HasLimit G] : (CategoryTheory.Limits.colimitLimitToLimitColimitCone G).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colim.map (CategoryTheory.Limits.limitIsoSwapCompLim G).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitLimitToLimitColimit (CategoryTheory.Functor.uncurry.obj G)) (CategoryTheory.Limits.lim.map (CategoryTheory.Functor.whiskerRight (CategoryTheory.Functor.currying.unitIso.app G).inv CategoryTheory.Limits.colim)))
• CategoryTheory.Limits.ι_colimitLimitToLimitColimit_π_apply 📋 Mathlib.CategoryTheory.Limits.ColimitLimit
  {J : Type u₁} {K : Type u₂} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.Category.{v₂, u₂} K] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor (J × K) C) [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape K C] (j : J) (k : K) {F✝ : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F✝ X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F✝] (x : carrier (((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp F)).comp CategoryTheory.Limits.lim).obj k)) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj F).comp CategoryTheory.Limits.colim) j)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimitLimitToLimitColimit F)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp F)).comp CategoryTheory.Limits.lim) k)) x)) = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj F).obj j) k)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp F)).obj k) j)) x)
• CategoryTheory.Limits.colimitLimitToLimitColimit_isIso 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
  {J : Type u₁} {K : Type u₂} [CategoryTheory.SmallCategory J] [CategoryTheory.Category.{v₂, u₂} K] [Small.{v, u₂} K] [CategoryTheory.FinCategory J] (F : CategoryTheory.Functor (J × K) (Type v)) [CategoryTheory.IsFiltered K] : CategoryTheory.IsIso (CategoryTheory.Limits.colimitLimitToLimitColimit F)
• CategoryTheory.Limits.comp_lim_obj_ext 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
  {J : Type u₁} {K : Type u₂} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.Category.{v₂, u₂} K] [Small.{v, u₂} K] {j : J} {G : CategoryTheory.Functor J (CategoryTheory.Functor K (Type v))} (x y : (G.comp CategoryTheory.Limits.lim).obj j) (w : ∀ (k : K), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π (G.obj j) k)) x = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π (G.obj j) k)) y) : x = y
• CategoryTheory.Limits.comp_lim_obj_ext_iff 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
  {J : Type u₁} {K : Type u₂} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.Category.{v₂, u₂} K] [Small.{v, u₂} K] {j : J} {G : CategoryTheory.Functor J (CategoryTheory.Functor K (Type v))} {x y : (G.comp CategoryTheory.Limits.lim).obj j} : x = y ↔ ∀ (k : K), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π (G.obj j) k)) x = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π (G.obj j) k)) y
• CategoryTheory.Limits.colimitLimitToLimitColimit_injective 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
  {J : Type u₁} {K : Type u₂} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.Category.{v₂, u₂} K] [Small.{v, u₂} K] (F : CategoryTheory.Functor (J × K) (Type v)) [CategoryTheory.IsFiltered K] [Finite J] : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimitLimitToLimitColimit F))
• CategoryTheory.Limits.colimitLimitToLimitColimit_surjective 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
  {J : Type u₁} {K : Type u₂} [CategoryTheory.SmallCategory J] [CategoryTheory.Category.{v₂, u₂} K] [Small.{v, u₂} K] [CategoryTheory.FinCategory J] (F : CategoryTheory.Functor (J × K) (Type v)) [CategoryTheory.IsFiltered K] : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimitLimitToLimitColimit F))
• CategoryTheory.Localization.HasProductsOfShapeAux.inverts 📋 Mathlib.CategoryTheory.Localization.FiniteProducts
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] (J : Type) [CategoryTheory.Limits.HasProductsOfShape J C] [W.IsStableUnderProductsOfShape J] : (W.functorCategory (CategoryTheory.Discrete J)).IsInvertedBy (CategoryTheory.Limits.lim.comp L)
• CategoryTheory.Localization.HasProductsOfShapeAux.instCatCommSqFunctorDiscreteLimObjWhiskeringRightLimitFunctor 📋 Mathlib.CategoryTheory.Localization.FiniteProducts
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] (J : Type) [CategoryTheory.Limits.HasProductsOfShape J C] [W.IsStableUnderProductsOfShape J] [W.ContainsIdentities] [Finite J] : CategoryTheory.CatCommSq CategoryTheory.Limits.lim ((CategoryTheory.Functor.whiskeringRight (CategoryTheory.Discrete J) C D).obj L) L (CategoryTheory.Localization.HasProductsOfShapeAux.limitFunctor L W J)
• CategoryTheory.Localization.HasProductsOfShapeAux.compLimitFunctorIso 📋 Mathlib.CategoryTheory.Localization.FiniteProducts
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] (J : Type) [CategoryTheory.Limits.HasProductsOfShape J C] [W.IsStableUnderProductsOfShape J] [W.ContainsIdentities] [Finite J] : ((CategoryTheory.Functor.whiskeringRight (CategoryTheory.Discrete J) C D).obj L).comp (CategoryTheory.Localization.HasProductsOfShapeAux.limitFunctor L W J) ≅ CategoryTheory.Limits.lim.comp L
• CategoryTheory.Localization.HasProductsOfShapeAux.adj_counit_app 📋 Mathlib.CategoryTheory.Localization.FiniteProducts
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] (J : Type) [CategoryTheory.Limits.HasProductsOfShape J C] [W.IsStableUnderProductsOfShape J] [W.ContainsIdentities] [Finite J] (F : CategoryTheory.Functor (CategoryTheory.Discrete J) C) : (CategoryTheory.Localization.HasProductsOfShapeAux.adj L W J).counit.app (F.comp L) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.const (CategoryTheory.Discrete J)).map ((CategoryTheory.Localization.HasProductsOfShapeAux.compLimitFunctorIso L W J).hom.app F)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.compConstIso (CategoryTheory.Discrete J) L).hom.app (CategoryTheory.Limits.lim.obj F)) (CategoryTheory.Functor.whiskerRight (CategoryTheory.Limits.constLimAdj.counit.app F) L))
• CategoryTheory.Limits.instLaxMonoidalFunctorLim 📋 Mathlib.CategoryTheory.Monoidal.Limits.Basic
  {J : Type w} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Limits.lim.LaxMonoidal
• CategoryTheory.Limits.lim_ε_π 📋 Mathlib.CategoryTheory.Monoidal.Limits.Basic
  {J : Type w} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.MonoidalCategory C] (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Limits.lim) (CategoryTheory.Limits.limit.π (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor J C)) j) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
• CategoryTheory.Limits.lim_ε_π_assoc 📋 Mathlib.CategoryTheory.Monoidal.Limits.Basic
  {J : Type w} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.MonoidalCategory C] (j : J) {Z : C} (h : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor J C)).obj j ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Limits.lim) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor J C)) j) h) = h
• CategoryTheory.Limits.lim_μ_π 📋 Mathlib.CategoryTheory.Monoidal.Limits.Basic
  {J : Type w} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.MonoidalCategory C] (F G : CategoryTheory.Functor J C) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Limits.lim F G) (CategoryTheory.Limits.limit.π (CategoryTheory.MonoidalCategoryStruct.tensorObj F G) j) = CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.Limits.limit.π F j) (CategoryTheory.Limits.limit.π G j)
• CategoryTheory.Limits.lim_μ_π_assoc 📋 Mathlib.CategoryTheory.Monoidal.Limits.Basic
  {J : Type w} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.MonoidalCategory C] (F G : CategoryTheory.Functor J C) (j : J) {Z : C} (h : (CategoryTheory.MonoidalCategoryStruct.tensorObj F G).obj j ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Limits.lim F G) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.MonoidalCategoryStruct.tensorObj F G) j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.Limits.limit.π F j) (CategoryTheory.Limits.limit.π G j)) h
• CategoryTheory.Sheaf.ΓNatIsoLim 📋 Mathlib.CategoryTheory.Sites.GlobalSections
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂) [CategoryTheory.Category.{v₂, u₂} A] [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.Limits.HasLimitsOfShape Cᵒᵖ A] : CategoryTheory.Sheaf.Γ J A ≅ (CategoryTheory.sheafToPresheaf J A).comp CategoryTheory.Limits.lim
• LightCondensed.instPreservesEpimorphismsFunctorDiscreteNatLightCondModLim 📋 Mathlib.Condensed.Light.Epi
  {R : Type u} [Ring R] : CategoryTheory.Limits.lim.PreservesEpimorphisms

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c