-
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(metric_space): add lipschitz_on_with #4151
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.
Maybe you don't need to copy the whole lipschitz API yet, but at least including lipschitz_on.continuous_on
and lipschitz_on_univ
(saying that lipschitz_on univ
is the same as lipschitz
) seems necessary. Also add a line on this in the file docstring.
358e23e
to
baf1e5c
Compare
I proved your minimal API lemmas, filling a couple of weird holes on the way. But writing this makes me wonder whether I should switch the argument order between the function and the set. It sounded more natural to me that way, but it's opposite to the |
Can you change the order of variables to match that of |
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.
Thanks 🎉
bors merge
The order of the explicit arguments in this definition is open for negotiation. From the sphere eversion project. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Pull request successfully merged into master. Build succeeded: |
The order of the explicit arguments in this definition is open for negotiation.
From the sphere eversion project.