mathlib

4e603f4b - feat(geometry/manifold/charted_space): typeclass `closed_under_restriction` for structure groupoids (#3347)

feat(geometry/manifold/charted_space): typeclass `closed_under_restriction` for structure groupoids (#3347) * Define a typeclass `closed_under_restriction` for structure groupoids. * Prove that it is equivalent to requiring that the structure groupoid contain all local homeomorphisms equivalent to the restriction of the identity to an open subset. * Verify that `continuous_groupoid` and `times_cont_diff_groupoid` satisfy `closed_under_restriction`. * Show that a charted space defined by a single chart is `has_groupoid` for any structure groupoid satisfying `closed_under_restriction`. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Restriction.20in.20structure.20groupoid)