-
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] - chore(analysis/convex): move convex_on_norm
, change API
#13631
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.
When I wrote those lemmas I didn't know whether it was more practical to have the univ
version or the convex set version.
By the way, do you think we should have a convex_on ℝ s (dist z)
version?
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
I don't know either. I just fixed the inconsistency in API.
IMHO, we should add it whenever we need it. |
Thanks! bors merge |
* Move `convex_on_norm` from `specific_functions` to `topology`, use it to golf the proof of `convex_on_dist`. * The old `convex_on_norm` is now called `convex_on_univ_norm`. The new `convex_on_norm` is about convexity on any convex set. * Add `convex_on_univ_dist` and make `s : set E` an implicit argument in `convex_on_dist`. This way APIs about convexity of norm and distance agree.
Pull request successfully merged into master. Build succeeded: |
convex_on_norm
, change APIconvex_on_norm
, change API
convex_on_norm
fromspecific_functions
totopology
, use it to golf the proof ofconvex_on_dist
.convex_on_norm
is now calledconvex_on_univ_norm
. The newconvex_on_norm
is about convexity on any convex set.convex_on_univ_dist
and makes : set E
an implicit argument inconvex_on_dist
.This way APIs about convexity of norm and distance agree.