mathlib3

361aa777 - feat(category_theory/adjunction): complete well-powered category with a coseparating set is cocomplete (#15988)

feat(category_theory/adjunction): complete well-powered category with a coseparating set is cocomplete (#15988) This corollary of the special adjoint functor theorem immediately implies that Grothendieck categories are complete, which, according to the Wikipedia article on Grothendieck categories, is "a rather deep result".