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/normed_space/normed_group_hom): remove bound_by #7860
Conversation
@@ -522,9 +516,6 @@ hg.comp hf | |||
lemma norm_noninc_of_isometry (hf : isometry f) : f.norm_noninc := | |||
λ v, le_of_eq $ norm_eq_of_isometry hf v | |||
|
|||
lemma bound_by_one_of_isometry (hf : isometry f) : f.bound_by 1 := |
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.
Should this instead be replaced by norm_le_one_of_isometry
?
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.
There is norm_noninc_of_isometry
that combined with norm_noninc_iff_norm_le_one
gives what you want.
It depends if we prefer to state lemmas about f.norm_noninc
or about ∥f∥ ≤ 1
(or both of course).
bors r+ |
`bound_by f C` is the same as `∥f∥ ≤ C` and it is therefore useless now that we have `∥f∥`.
This PR was included in a batch that successfully built, but then failed to merge into master (it was a non-fast-forward update). It will be automatically retried. |
`bound_by f C` is the same as `∥f∥ ≤ C` and it is therefore useless now that we have `∥f∥`.
Build failed (retrying...): |
`bound_by f C` is the same as `∥f∥ ≤ C` and it is therefore useless now that we have `∥f∥`.
Pull request successfully merged into master. Build succeeded: |
bound_by f C
is the same as∥f∥ ≤ C
and it is therefore useless now that we have∥f∥
.