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(analysis/normed_space): normed group hom completion #8499
Conversation
9389961
to
a76e6ef
Compare
🎉 Great news! Looks like all the dependencies have been resolved:
💡 To add or remove a dependency please update this issue/PR description. Brought to you by Dependent Issues (:robot: ). Happy coding! |
a76e6ef
to
63e918f
Compare
lemma normed_group_hom.completion_def (f : normed_group_hom G H) (x : completion G) : | ||
f.completion x = completion.map f x := rfl | ||
|
||
lemma normed_group_hom.completion_coe_to_fun (f : normed_group_hom G H) : |
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.
can you make this one a simp lemma (and then probably the simp attribute on the next one is not needed any more)?
(h : f.surjective_on_with f.range C) : | ||
(f.completion.ker : set $ completion G) = closure (to_compl.comp $ incl f.ker).range := | ||
begin | ||
by_cases Hf : ∀ x, ∥f x∥ = 0, -- This is a bit silly, we simply avoid assuming C ≥ 0 |
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.
couldn't you instead have a general lemma saying that, if f.surjective_on_with f.range C
, then there exists a positive D
such that f.surjective_on_with f.range D
? Or even surjective_on_with.mono
, saying that if it works for C
then it works for any D \ge C
?
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.
Great idea, thanks!
bors r+ |
Pull request successfully merged into master. Build succeeded: |
From LTE
This used to be part of #8317