Documentation

Mathlib.CategoryTheory.Limits.EssentiallySmall

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.

See also the file FinallySmall.lean for more general results.