-
Notifications
You must be signed in to change notification settings - Fork 299
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(geometry/manifold/charted_space): open subset of a manifold is a manifold #3442
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This looks great, thanks! I just have a few minor comments left.
bors d+
✌️ hrmacbeth can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
bors r+ |
… 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.
bors r+ |
… 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.
Pull request successfully merged into master. Build succeeded: |
An open subset of a charted space is naturally a charted space. If the charted space has structure groupoid
G
(withG
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 isuniv
is an open embedding, and conversely.I wrote this as an exercise in the
local_homeomorph
lemmas. Feel free to close this PR if it doesn't fit well in the library (for example, if it should follow later from more general theory).