mathlib

431589bc - feat(geometry/manifold/sheaf/basic): sheaf of functions satisfying a `local_invariant_prop` (#19146)

feat(geometry/manifold/sheaf/basic): sheaf of functions satisfying a `local_invariant_prop` (#19146) 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).