I just had a student come to my office hours and ask me a ton of questions, the answer to all of which was "that's a slight variant to the implicit function theorem, which is proved by formal manipulation from the implicit function theorem". For example: 


$\def\RR{\mathbb{R}}$ Let $f : \RR^n \to \RR$ be a smooth function and suppose that $\partial f/ \partial x\_n \neq 0$. Then, locally, $(x\_1, x\_2, \ldots, x\_{n-1}, f)$ are coordinates on $\RR^n$.


Let $f : \RR^n \to \RR$ be a smooth function and suppose that $\partial f/ \partial x\_n \neq 0$. Then, locally, $(x\_1, x\_2, \ldots, x\_{n-1})$ are coordinates on $\{ f=0 \}$.


Let $U$ be a small open set in $\RR^d$ and let $(f\_1, \ldots, f\_d): U \to \RR^n$ parameterize a patch on a manifold $M$ in $\RR^n$. Suppose that $\det (\partial f\_i/\partial x\_j)\_{1 \leq i,j \leq d} \neq 0$. Then $x\_1$, ..., $x\_d$ are local coordinates on $M$.


Let $g\_1$, ..., $g\_{n-d}$ be smooth functions $\RR^n \to \RR$. Let $M= \{g\_1=g\_2=\ldots=g\_{n-d} = 0 \}$. Suppose that $\det (\partial f\_i/\partial x\_j)\_{1 \leq i,j \leq n-d} \neq 0$. Then $M$ is a smooth manifold of dimension $d$ and $x\_{n-d+1}$, ..., $x\_n$ are local coordinates near $0$.



> 
> Does anyone know a book which works
>  through these sort of variants
>  systematically?
> 
> 
> 


I should mention that I actually need these facts for holomorphic functions. But I have a good reference for the holomorphic implicit function theorem: Gunning and Rossi, Chapter 1. The problem is that I want a reference which goes slowly through these variants, rather than assuming they are obvious corollaries.



Reference for working with the implicit function theorem
Shameless plug: In [my thesis](https://arxiv.org/abs/1909.00744), I introduced the following notion of an (abstract) normal form. It consists of a tuple $(X, Y, \hat{f}, f\_s)$ where:


* $X$ and $Y$ finite-dimensional vector spaces with compositions $X = Ker \oplus Coim$ and $Y = Coker \oplus Im$,
* $\hat{f}: Coim \to Im$ is a linear isomorphism,
* $f\_s: X \to Coker$ is a smooth map with vanishing derivative at $0$ which satisfies $f\_s(0, x) = 0$ for all $x \in Coim$.


The inverse function theorem can then be used to show that every smooth map $f: M \to N$ can be brought into such a normal form, i.e. there exist charts such that $f$ locally coincides with $\hat{f} + f\_s$. The abstract spaces $Ker$, $Coimg$, $Coker$ and $Im$ in the normal form are then of course identified with the corresponding kernel, coimage, ... of the derivative of $f$. This normal form theorem has the immersion, the submersion and the constant rank theorem as direct corollaries, and it also serves as the natural "parent" for all your statements.


For example consider the second statement.



> 
> Let $f : \mathbb R^n \to \mathbb R$ be a smooth function and suppose that $\partial f/ \partial x\_n \neq 0$. Then, locally, $(x\_1, x\_2, \ldots, x\_{n-1})$ are coordinates on $\{ f=0 \}$.
> 
> 
> 


Proof: Since $\partial f/ \partial x\_n \neq 0$, we have $Ker = span (x\_1, \dots, x\_{n\_1})$, $Coimg = span (x\_n)$, $Img = \mathbb R$ and trivial $Coker$. Moreover, $f$ is locally given by a linear isomorphism $\hat{f}: Coimg \to Img$ so that $\{f = 0\}$ is identified with $Ker = span (x\_1, \dots, x\_{n\_1})$.


