-
Notifications
You must be signed in to change notification settings - Fork 257
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: locally Lipschitz maps #7314
Conversation
Two sorries related to coercions remain.
…schitz. And some small golfs using dot notation.
For the proof of composition, I'm stuck on two sorries related to coercions of subsets. Minimized code:
|
enables dot notation and golfing some proofs quite a bit more.
@eric-wieser Thanks for the quick comments. I've made the requested changes. |
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Fixed the last sorry - courtesy of Alex J. Best on zulip. Thanks! |
Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>
And slight tweaks to the doc comments, and a minigolf using dot notation.
474b489
to
0ce2603
Compare
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
awaiting-review |
bors d+ |
✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with |
Thanks for the review! |
Define locally Lipschitz maps and show their basic properties. In particular, they are continuous and stable under composition and products. As an application, we conclude that C¹ maps are locally Lipschitz. Co-authored-by: grunweg <grunweg@posteo.de>
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. |
Define locally Lipschitz maps and show their basic properties.
In particular, they are continuous and stable under composition and products.
As an application, we conclude that C¹ maps are locally Lipschitz.
I've gone through the entire file; all API for Lipschitz maps (where this makes sense) has a counterpart for locally Lipschitz maps.
Left for the future:
(hence, locally Lipschitz functions form a submodule of the ring of continuous functions)