Inverse function theorem

Before getting started, let us go back on some definitions:

Definition. Let U be an open subset of Rn and let f:UVRn be a C1-mapping, then f is a C1-diffeomorphism or globally invertible if and only if there exists g:VU a C1-mapping such that:

fg=idV and gf=idU.

In other words, f is a bijection whose inverse is smooth. This is not to be confused with:

Definition. The mapping f is said to be a local diffeomorphism or locally invertible if and only if when restricted to an open subset of U, f is a diffeomorphism onto its image.

Please notice that being locally invertible around any point does not imply being globally invertible.

Theorem. Let U be an open subset of Rn, let x be a point of U and let f:URn be a C1-mapping. Assume that dxf:RnRn is an invertible linear map, then there exists V an open neighbourhood of x such that f:Vf(V) is a C1-diffeomorphism.