Inverse function theorem

Let $𝑈 \subseteq ℝ 𝑛$ be open, $𝐹 : 𝑈 \to ℝ 𝑛$ be $𝐶 \infty$ differentiable, and $𝑥 \in 𝑈$ . Then if the total derivative $𝐷 𝐹 (𝑥)$ is non-singular, there exist open neighbourhoods $𝑈'$ of $𝑥$ in $𝑈$ and $𝑉$ of $𝑓 (𝑥)$ in $ℝ 𝑛$ such that

𝐹 ↾ 𝑈' : 𝑈' \to 𝑉

is a $𝐶 \infty$ diffeomorphism, #m/thm/anal i.e. $𝐹$ is locally a diffeomorphism at $𝑥$ .

Proof

#missing/proof

The constructive proof relates to Newton's method.

Corollary

The above theorem is easily extended to a $𝐶 \infty$ differentiable map $𝑓 : 𝑋 \to 𝑌$ between $𝐶 \infty$ differentiable manifolds $𝑋, 𝑌$ . If the Tangent map $𝑇 𝑥 𝑓 : 𝑇 𝑥 𝑋 \to 𝑇 𝑓 (𝑥) 𝑌$ is a Linear isomorphism, then $𝑓$ is a local diffeomorphism, as one expects from the Linearization dogma.

#state/develop | #lang/en | #SemBr