Commit 2021-02-14 23:17 6f99407e

feat(analysis/calculus/inverse): a function with onto strict derivative 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.