Boundary of a Smooth Manifold with Boundary as a Smooth Manifold of Dimension n-1

Let $n\in$ $\mathbb{N}$ with $n\ge 2$, and let $M$ be a smooth manifold with boundary of dimension $n$ whose boundary $\partial M$ is nonempty. Give $\partial M$ the subspace topology inherited from $M$. Then the following hold.

1. $\partial M$ is a closed subset of $M$.

2. With the subspace topology, $\partial M$ is Hausdorff and second countable.

3. Let $(U,\varphi)$ be a chart in the chosen atlas of $M$ with $U\cap\partial M\ne\varnothing$. Then $\varphi(U\cap\partial M)=\varphi(U)\cap\partial H^n$, where $\partial H^n$ is the boundary hyperplane of the closed upper half-space. Let $\pi:\mathbb{R}^n\to\mathbb{R}^{n-1}$, between Euclidean spaces, denote the projection $\pi(x_1,\dots,x_n)=(x_1,\dots,x_{n-1})$, and for $c\in\mathbb{R}^{n-1}$ let $T_c:\mathbb{R}^{n-1}\to\mathbb{R}^{n-1}$ denote the translation $T_c(y)=y+c$. Then for every $p\in U\cap\partial M$ there exist an open subset $U'$ of $M$ with $p\in U'\subseteq U$ and a vector $c\in\mathbb{R}^{n-1}$ such that the pair $(U'\cap\partial M,\psi)$, with chart map $\psi=T_c\circ\pi\circ\varphi$ restricted to $U'\cap\partial M$, is a chart of dimension $n-1$ on $\partial M$ whose image is contained in the set of points $y=(y_1,\dots,y_{n-1})$ of the closed upper half-space $H^{n-1}$ with $y_{n-1}>0$. Charts of this form are called induced boundary charts of $\partial M$.

4. Any two induced boundary charts are smoothly compatible, and the collection of all induced boundary charts is a smooth atlas of dimension $n-1$ on $\partial M$, making $\partial M$ a smooth manifold with boundary of dimension $n-1$ in which every point is an interior point in the sense of Interior Points, Boundary Points, and Boundary of a Smooth Manifold with Boundary; that is, the boundary of $\partial M$ is empty.

5. If $M$ is compact in the sense of Smooth Atlas and Smooth Manifold with Boundary, then $\partial M$ is compact, by claim 1 together with Closed Subset of a Compact Space is Compact.