[Merged by Bors] - feat(analysis/normed/group/basic): norm lemmas for lipschitz and antilipschitz #19103
Conversation
…lipschitz This also corrects some nonsense names produced by to_additive.
eric-wieser
added
awaiting-review
There was a problem hiding this comment.
I'm really surprised we don't have those lemmas. But they are indeed missing, LGTM.
@urkud, could you check?
github-actions
bot
removed
the
awaiting-CI
src/analysis/normed/group/basic.lean
Outdated
| lemma antilipschitz_with.le_mul_nnnorm' {f : E → F} | ||
| {K : ℝ≥0} (h : antilipschitz_with K f) (hf : f 1 = 1) (x) : ‖x‖₊ ≤ K * ‖f x‖₊ := | ||
| h.le_mul_norm' hf x | ||
|
|
||
| @[to_additive] lemma monoid_hom_class.bound_of_antilipschitz [monoid_hom_class 𝓕 E F] (f : 𝓕) |
There was a problem hiding this comment.
While you're at it, could you please generalize to map_one_class? Do you need the new lemmas for unbundled functions? Anyway, LGTM.
bors d+
There was a problem hiding this comment.
Done. Yes, I think I wanted this for unbundled functions, though I no longer remember why.
|
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
urkud
added
delegated
|
bors merge |
github-actions
bot
added
the
ready-to-merge
…lipschitz (#19103) This also corrects some nonsense names produced by to_additive.
|
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. |
bors
bot
changed the title
This also corrects some nonsense names produced by to_additive.