mathlib

fb7698eb - feat(topology/sheaves): Locally surjective maps of presheaves (#15398)

feat(topology/sheaves): Locally surjective maps of presheaves (#15398) For presheaves valued in a concrete category, we define locally surjective maps of presheaves and show that this condition is equivalent to all the induced maps of stalks being surjective. We also introduce notation for the types of sections, germs and corresponding induced maps. Co-authored by: Sam van Gool @samvang Co-authored-by: erd1 <the.erd.one@gmail.com> Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>