Commit 2020-07-19 21:18 953ab3ab

feat(geometry/manifold/charted_space): open subset of a manifold is a manifold (#3442) An open subset of a charted space is naturally a charted space. If the charted space has structure groupoid G (with G closed under restriction), then the open subset does also. Most of the work is in topology/local_homeomorph, where it is proved that a local homeomorphism whose source is univ is an open embedding, and conversely.