> [!theorem] > > Let $X$ and $Y$ be $C^p$-[[Manifold|manifolds]] ($p \ge 1$) and $f: X \to Y$ be a $C^p$-[[Manifold Morphism|morphism]]. If there exists $p \in X$ such that the [[Differential|differential]] $df_p$ is a [[Space of Toplinear Isomorphisms|toplinear isomorphism]], there exists [[Open Set|open]] [[Neighbourhood|neighbourhoods]] $U_0 \in \cn^o(p)$ and $V_0 \in \cn^o(f(p))$ such that $f|_{U_0}$ is a $C^p$-[[Diffeomorphism|diffeomorphism]]. > > *Proof*. Let $(U, \psi) \in X$ and $(V, \varphi) \in Y$ be [[Atlas|charts]] with $p \in U$ and $f(p) \in V$. Since $df_p$ is a toplinear isomorphism, so is the [[Derivative|derivative]] $D(f_{U, V})(p)$. By the [[Inverse Function Theorem]], there exists a neighbourhood $\widehat{U'} \in \cn^o(\hat{p})$ such that $f_{U, V}|_{\widehat{U'}}$ is a $C^p$-isomorphism. Therefore $f|_{U'}$ where $U' = \psi^{-1}(\widehat{U'})$ is a $C^p$-diffeomorphism.