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/calculus/inverse): a function with onto strict derivative is locally onto #6229
Conversation
end | ||
|
||
/-- A surjective continuous linear map admits a (possibly nonlinear) controlled right inverse. | ||
In general, it is not possible to ensure that such a right inverse is linear. -/ |
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.
Could you please add "between Banach spaces"?
src/analysis/calculus/inverse.lean
Outdated
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. | |||
Authors: Yury Kudryashov, Heather Macbeth. |
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.
Authors: Yury Kudryashov, Heather Macbeth. | |
Authors: Yury Kudryashov, Heather Macbeth, Sébastien Gouëzel. |
Thanks! |
✌️ sgouezel can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
…ve is locally onto (#6229) Removes a useless assumption in `map_nhds_eq_of_complemented` (no need to have a completemented subspace). The proof of the local inverse theorem breaks into two parts, local injectivity and local surjectivity. We refactor the local surjectivity part, assuming in the proof only that the derivative is onto. The result is stronger, but the proof is less streamlined since there is no contracting map any more: we give a naive proof from first principles instead of reducing to the fixed point theorem for contracting maps.
Pull request successfully merged into master. Build succeeded: |
…ve is locally onto (#6229) Removes a useless assumption in `map_nhds_eq_of_complemented` (no need to have a completemented subspace). The proof of the local inverse theorem breaks into two parts, local injectivity and local surjectivity. We refactor the local surjectivity part, assuming in the proof only that the derivative is onto. The result is stronger, but the proof is less streamlined since there is no contracting map any more: we give a naive proof from first principles instead of reducing to the fixed point theorem for contracting maps.
Removes a useless assumption in
map_nhds_eq_of_complemented
(no need to have a completemented subspace).The proof of the local inverse theorem breaks into two parts, local injectivity and local surjectivity. We refactor the local surjectivity part, assuming in the proof only that the derivative is onto. The result is stronger, but the proof is less streamlined since there is no contracting map any more: we give a naive proof from first principles instead of reducing to the fixed point theorem for contracting maps.