mathlib

8c1fa705 - feat(category_theory/limits/concrete_category): Some lemmas about filtered colimits (#10270)

feat(category_theory/limits/concrete_category): Some lemmas about filtered colimits (#10270) This PR adds some lemmas about (filtered) colimits in concrete categories which are preserved under the forgetful functor. This will be used later for the sheafification construction.