mathlib3

0cc93a13 - feat(category_theory/is_filtered): is_filtered_of_equiv (#5485)

feat(category_theory/is_filtered): is_filtered_of_equiv (#5485) If `C` is filtered and there is a right adjoint functor `C => D`, then `D` is filtered. Also a category equivalent to a filtered category is filtered. Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>