mathlib3

7e6393f8 - feat(topology/sheaves): the sheaf condition for functions satisfying a local predicate (#3906)

feat(topology/sheaves): the sheaf condition for functions satisfying a local predicate (#3906) Functions satisfying a local predicate form a sheaf. This sheaf has a natural map from the stalk to the original fiber, and we give conditions for this map to be injective or surjective. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>