mathlib

c363ad63 - feat(category_theory/sites/*): Cover preserving functors (#9691)

feat(category_theory/sites/*): Cover preserving functors (#9691) Split from #9650 - Defined `cover_preserving` functors as functors that push covering sieves to covering sieves. - Defined `compatible_preserving` functors as functors that push compatible families to compatible families. - Proved that functors that are both `cover_preserving` and `compatible_preserving` pulls sheaves to sheaves. Co-authored-by: erdOne <36414270+erdOne@users.noreply.github.com>