Commit 2020-07-12 07:43 4e603f4b

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