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/banach): a range with closed complement is itself closed #6972
Conversation
src/linear_algebra/prod.lean
Outdated
ker (f.coprod g) = (ker f).prod (ker g) := | ||
begin | ||
ext x, | ||
rcases x with ⟨y, z⟩, |
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.
AFAIR, you can use ext ⟨y, z⟩
. Also, one of the inequalities hold without hd
. Could you please add it as a separate lemma?
Otherwise LGTM |
✌️ sgouezel can now approve this pull request. To approve and merge a pull request, simply reply with |
@sgouezel ping? |
bors r+ |
… itself closed (#6972) If the range of a continuous linear map has a closed complement, then it is itself closed. For instance, the range can not be a dense hyperplane. We prove it when, additionally, the map has trivial kernel. The general case will follow from this particular case once we have quotients of normed spaces, which are currently only in Lean Liquid. Along the way, we fill several small gaps in the API of continuous linear maps.
Pull request successfully merged into master. Build succeeded: |
If the range of a continuous linear map has a closed complement, then it is itself closed. For instance, the range can not be a dense hyperplane. We prove it when, additionally, the map has trivial kernel. The general case will follow from this particular case once we have quotients of normed spaces, which are currently only in Lean Liquid.
Along the way, we fill several small gaps in the API of continuous linear maps.