mathlib

edf07cfb - feat(topology/sheaves/sheaf_condition/sites): Connect sheaves on sites to sheaves on spaces (#9609)

feat(topology/sheaves/sheaf_condition/sites): Connect sheaves on sites to sheaves on spaces (#9609) Show that a sheaf on the site `opens X` is the same thing as a sheaf on the space `X`. This finally connects the theory of sheaves on sites to sheaves on spaces, which were previously independent of each other.