# mathlibdocumentation

category_theory.limits.essentially_small

# Limits over essentially small indexing categories #

If C has limits of size w and J is w-essentially small, then C has limits of shape J.

theorem category_theory.limits.has_products_of_shape_of_small (C : Type u₁) (β : Type w₂) [small β]  :
theorem category_theory.limits.has_coproducts_of_shape_of_small (C : Type u₁) (β : Type w₂) [small β]  :