Commit 2020-09-20 21:53 db9842c8
View on Github →feat(analysis/calculus/times_cont_diff): inversion of continuous linear maps is smooth (#4185)
- Introduce an
inverse
function on the space of continuous linear maps between two Banach spaces, which is the inverse if the map is a continuous linear equivalence and zero otherwise. - Prove that this function is
times_cont_diff_at
eachcontinuous_linear_equiv
. - Some of the constructions used had been introduced in #3282 and placed in
analysis.normed_space.operator_norm
(normed spaces); they are moved to the earlier filetopology.algebra.module
(topological vector spaces).