Let $E, F$ be Banach spaces over $\mathbb{K} \in \{\mathbb{C}, \mathbb{R}\}$. Let $\mathcal L_{\text{is}} (E, F)$ be the set of all topological isomorphisms from $E$ to $F$. Then $\mathcal L_{\text{is}} (E, F)$ is an open subset of the Banach space $\mathcal L(E, F)$ of continuous linear functions from $E$ to $F$.
I'm reading inverse function theorems in Amann's Analysis I,II, i.e.,
1.8 Theorem (differentiability of inverse functions) Suppose $X \subset \mathbb{K}$ and $a \in X$ is a limit point of $X$. Let $f:X \to \mathbb K$ be injective and consider the inverse $f^{-1}: Y \rightarrow X$ of $f$ where $Y:=f(X)$. Suppose that $f$ is differentiable at $a$, and $f^{-1}$ is continuous at $b:=f(a) \in Y$. Then
- $b$ is a limit point of $Y$.
- $f^{-1}$ is differentiable at $b$ if and only if $f^{\prime}(a) \neq 0$. In this case, $\left(f^{-1}\right)^{\prime}(b)=1 / f^{\prime}(a)$.
and
7.3 Theorem (inverse function) Suppose $X$ is open in $E$ and $a \in X$. Also suppose for $q \in \mathbb{N}^{*} \cup\{\infty\}$ that $f \in C^q(X, F)$. Finally, suppose $\partial f\left(a\right) \in \mathcal L_{\text{is}}(E, F)$. Then there is an open neighborhood $U$ of $a$ in $X$ and an open neighborhood $V$ of $b:=f\left(a\right)$ in $F$ with these properties:
- $f: U \rightarrow V$ is bijective.
- $f^{-1} \in C^q(V, E)$, and for every $x \in U$, we have $\partial f(x) \in \mathcal L_{\text{is}}(E, F)$ and $\partial f^{-1}(f(x))=[\partial f(x)]^{-1}$.
Here $a \in E$ is a limit point of $X$ if every neighborhood of $a$ in $E$ contains an element of $X$ other than $a$. Theorem 1.8 concerns differentiable functions in $1$D, whereas Theorem 7.3 concerns continuously differentiable functions in infinite dimension.
I would like to ask if below result, concerning differentiable functions in infinite dimension, holds. It is some kind of average of Theorem 1.8 and Theorem 7.3.
Suppose $X \subset E$ and $a \in X$ is a limit point of $X$. Let $f:X \to F$ be injective and consider the inverse $f^{-1}: Y \rightarrow X$ of $f$ where $Y := f(X)$. Suppose that $f$ is differentiable at $a$ and $f^{-1}$ is continuous at $b :=f(a) \in Y$. Then
- $b$ is a limit point of $Y$.
- $f^{-1}$ is differentiable at $b$ if and only if $\partial f\left(a\right) \in \mathcal L_{\text{is}}(E, F)$. In this case, $\partial f^{-1}(b)=[\partial f(a)]^{-1}$.
Thank you so much for your help!