Limits over essentially small indexing categories #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
C has limits of size
w-essentially small, then
C has limits of shape
theorem category_theory.limits.has_products_of_shape_of_small (C : Type u₁) [category_theory.category C] (β : Type w₂) [small β] [category_theory.limits.has_products C] :
theorem category_theory.limits.has_coproducts_of_shape_of_small (C : Type u₁) [category_theory.category C] (β : Type w₂) [small β] [category_theory.limits.has_coproducts C] :