mathlib

64abe5aa - feat(category_theory/sites): closed sieves (#5282)

feat(category_theory/sites): closed sieves (#5282) - closed sieves - closure of a sieve - subobject classifier in Sheaf (without proof of universal property) - equivalent sheaf condition iff same topology - closure operator induces topology