[Merged by Bors] - feat(geometry/manifold/sheaf/basic): sheaf of functions satisfying a `local_invariant_prop`

[hrmacbeth]

Define structure_groupoid.local_invariant_prop.sheaf, the sheaf-of-types of functions f : M → M' (for charted spaces M, M') satisfying some local property in the sense of structure_groupoid.local_invariant_prop (for example continuity, differentiability, smoothness).

---

[bors[bot]]

:v: hrmacbeth can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[hrmacbeth]

bors r+

[bors[bot]]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here. For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build mathlib
• Lint mathlib
• Lint style
• Run tests