I'm having difficulties proving lemma 3 of Milnor, Topology from the differentiable point of view. The lemma intends to give us a way to generate examples of mainfold with boundary. The lemma states the following:
Let $M$ be a smooth manifold without boundary and let $g:M \to \mathbb{R}$ have $0$ as regular value. The set of $x$ in $M$ with $g(x) \geq 0$ is a smooth manifold, with a boundary equal to $g^{-1}(0)$.
What I have so far:
I supposed $g$ is a smooth function because of the existence of regular value for $g$ and the general context of the book.
Because $g$ is smooth, $g^{-1}((0,+\infty))$ is open in $M$. Therefore, $g^{-1}((0,+\infty))$ is a smooth manifold of dimension $m$, as is $M$. By a preceding lemma, we know $g^{-1}(0)$ is a smooth manifold of dimension $m-1$. In that case, for every point $x \in g^{-1}(0)$ there exists an open neighborhood of $x$ diffeomorphic to an open set in $\mathbb{R}^{m-1}$.
To conclude:
To conclude the proof that $g^{-1}([0,+\infty))$ is a smooth manifold, I need to show that we can map with a diffeomorphism every small enought neighborhood in $g^{-1}([0,+\infty))$ to $V \cap H^{m}$, with the points of the boundary $g^{-1}(0)$ mapped to $\partial H^m$. Here, $H^m$ is the half-space $\{(x_1,...,x_m) \in \mathbb{R}^m\vert x_m \geq 0 \}$ and $V$ is an open set of $\mathbb{R}^m$.
I do not know how to proceed from here. Any help is greatly appreciated.
There are several ways of showing this; here's a sketch of one path:
Fix $p\in g^{-1}(\{0\})$. Since you have already showed that $g^{-1}(\{0\})$ is an embedded codimension $1$ submanifold, you can choose local coordinates $(x^1,\cdots,x^{n-1})$ with domain $U$, where $p\in U\subseteq g^{-1}(\{0\})$. Shrinking $U$ as necessary, we can arbitrarily extend the $x^i$ to smooth functions $M\to\mathbb{R}$. One can then use inverse function theorem to show that $(x^1,\cdots,x^{n-1},g)$ forms a coordinate chart on $M$ when restricted to a sufficiently small neighborhood of $p$, and restricting this map to $g^{-1}([0,\infty))$will give the desired boundary chart.