1: \begin{definition}[Banach Inverse Mapping Theorem]

2: Let $X,Y$ be computable Banach spaces. Then we define

3: \[\IMT_{X,Y}:\In\CC(X,Y)\to\CC(Y,X),T\mapsto T^{-1}\]

4: with $\dom(\IMT_{X,Y}):=\{T\in\CC(X,Y):T\mbox{ linear and bijective}\}$.

5: \end{definition}

6: