-
Notifications
You must be signed in to change notification settings - Fork 297
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): lemmas from the sphere eversion project #18877
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.
LGTM, thanks. Your note on composition clarified a behavior I had never fully understood!
bors d+
✌️ fpvandoorn 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 merge |
) * Also adds a new library note `comp_of_eq lemmas` about how (I think) we should better formulate composition lemmas of properties of functions. * About the library note `comp_of_eq lemmas`: exactly the same problems happen in Lean 4. * renamings ``` smooth_iff_proj_smooth -> smooth_prod_iff differentiable_at.fderiv_within_prod -> differentiable_within_at.fderiv_within_prod ``` * We add a `path_connected_space` instance of the tangent space. This instance is sufficient to compile sphere-eversion, without any `normed_space` instances on the tangent space (which are not the canonical structure on the tangent space). * From the sphere eversion project
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
Forward-port of leanprover-community/mathlib#18877 (2 files)
Forward-port of leanprover-community/mathlib#18877 (2 files)
comp_of_eq lemmas
about how (I think) we should better formulate composition lemmas of properties of functions.comp_of_eq lemmas
: exactly the same problems happen in Lean 4.path_connected_space
instance of the tangent space. This instance is sufficient to compile sphere-eversion, without anynormed_space
instances on the tangent space (which are not the canonical structure on the tangent space).