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

Step A (no point is both interior and boundary). Suppose $p\in M$ has charts $(U,\varphi)$ and $(V,\psi)$ in the atlas with $\varphi(p)\in\partial H^n$ and $\psi(p)\in\operatorname{int}(H^n)$, in the notation of Closed Upper Half-Space in Euclidean Space and Interior Points, Boundary Points, and Boundary of a Smooth Manifold with Boundary. Let $c=\psi(p)$. Since $\psi(U\cap V)$ is open in $H^n$ and $c\in\operatorname{int}(H^n)$, there is an open set $O\subseteq\mathbb{R}^n$ with $c\in O\subseteq\psi(U\cap V)\cap\operatorname{int}(H^n)$. Let $G:W\to W'$ be a local smooth extension of $\varphi\circ\psi^{-1}$ at $c$ and $F$ one of $\psi\circ\varphi^{-1}$ at $G(c)=\varphi(p)$, furnished by Smooth Compatibility of Charts Modeled on the Closed Upper Half-Space. On a neighborhood of $c$ inside $O$ we have $F\circ G=\mathrm{id}$ exactly (both transitions are honest maps there and on its image), so by C^1 Maps on Euclidean Open Sets are Differentiable and the chain rule, $J_F(G(c))\,J_G(c)$ is the identity matrix; hence $J_G(c)$ is invertible and, since an invertible matrix has nonzero determinant (were $\det J_G(c)=0$, its columns would be linearly dependent and $J_F(G(c))J_G(c)$ would annihilate a nonzero vector, contradicting invertibility of the identity), $\det J_G(c)\ne 0$. By the smooth inverse function theorem applied to $G$ restricted to an open neighborhood of $c$ contained in $O$, there are open sets $O'\ni c$ and $W''\ni\varphi(p)$ in $\mathbb{R}^n$ with $G(O')=W''$. But $G(O')=\varphi(\psi^{-1}(O'))\subseteq\varphi(U)\subseteq H^n$, and an open subset of $\mathbb{R}^n$ containing the point $\varphi(p)\in\partial H^n$ necessarily contains points with negative last coordinate, which do not lie in $H^n$. This contradiction proves Step A. Consequently, for every chart $(U,\varphi)$:

since a point of $U$ maps into $\partial H^n$ exactly when it is a boundary point.

Claim 1. If $p$ is an interior point with chart $(U,\varphi)$, then $\varphi^{-1}\bigl(\varphi(U)\cap\operatorname{int}(H^n)\bigr)$ is an open subset of $M$ (as $\varphi$ is a continuous bijection onto its image with continuous inverse, by Chart Modeled on the Closed Upper Half-Space, and $\operatorname{int}(H^n)$ is open) consisting of interior points and containing $p$. Hence $\operatorname{int}(M)$ is open, and by Step A, $\partial M=M\setminus\operatorname{int}(M)$ is a closed subset of $M$.

Claim 2. Directly from Subspace Topology: for distinct $p,q\in\partial M$ choose disjoint open sets of $M$ separating them (Hausdorff Topological Space) and intersect with $\partial M$; and intersecting the members of a countable basis of $M$ (Second Countable Topological Space) with $\partial M$ yields a countable basis of the subspace.

Claim 3. The first assertion is the display in Step A. In what follows, a homeomorphism onto its image means a bijection onto its image that is continuous with continuous inverse, for the relevant subspace topologies — the notion appearing in Chart Modeled on the Closed Upper Half-Space. The map $\pi$ restricted to $\partial H^n$ is a bijection onto $\mathbb{R}^{n-1}$ with inverse $y\mapsto(y,0)$; both directions are continuous, so $\pi$ restricts to a homeomorphism from $\partial H^n$ onto $\mathbb{R}^{n-1}$. Given $p\in U\cap\partial M$, let $B_1$ be the open ball of radius $1$ around $\varphi(p)$ for the Euclidean distance, and set $U'=\varphi^{-1}(B_1\cap\varphi(U))$, an open subset of $M$ with $p\in U'\subseteq U$ (using Open Ball in a Metric Space is Open and Euclidean Openness Agrees with Metric Openness on $\mathbb{R}^n$). Then $\varphi(U'\cap\partial M)=\varphi(U')\cap\partial H^n$ is open in $\partial H^n$, so $P=\pi(\varphi(U'\cap\partial M))$ is open in $\mathbb{R}^{n-1}$ and is contained in the radius-$1$ ball around $\pi(\varphi(p))$, hence bounded in the last coordinate. Choose $c=(0,\dots,0,t)$ with $t$ so large that $y_{n-1}+t>0$ for every $y\in P$. Then $\psi=T_c\circ\pi\circ\varphi$ restricted to $U'\cap\partial M$ is a composition of homeomorphisms onto their images, its image $T_c(P)$ is open in $\mathbb{R}^{n-1}$ and contained in the set of points of $H^{n-1}$ with $y_{n-1}>0$; such a set is open in $H^{n-1}$ in the sense of Closed Upper Half-Space in Euclidean Space. Hence $(U'\cap\partial M,\psi)$ is a chart of dimension $n-1$ on $\partial M$ with the stated image property.

Claim 4. Let $\psi_1=T_{c_1}\circ\pi\circ\varphi_1$ and $\psi_2=T_{c_2}\circ\pi\circ\varphi_2$ be induced boundary charts with overlapping domains, arising from charts $(U_1,\varphi_1)$, $(U_2,\varphi_2)$ of $M$. Fix $y$ in $\psi_1$ of the overlap and set $a=(T_{c_1}^{-1}(y),0)=\varphi_1(\psi_1^{-1}(y))\in\partial H^n$. Let $F:W\to W'$ be a local smooth extension of $\varphi_2\circ\varphi_1^{-1}$ at $a$ from Smooth Compatibility of Charts Modeled on the Closed Upper Half-Space. On the open set $\widetilde W=\{z\in\mathbb{R}^{n-1}:(T_{c_1}^{-1}(z),0)\in W\}$ define

Every partial derivative of $G$ of every order is the corresponding partial derivative of components of $F$ evaluated along an affine slice, hence exists and is continuous; so $G$ is smooth. For $z\in\widetilde W\cap\psi_1(\text{overlap})$, the point $q=\psi_1^{-1}(z)$ lies in $U_1\cap U_2\cap\partial M$, $\varphi_1(q)=(T_{c_1}^{-1}(z),0)$, and $F(\varphi_1(q))=\varphi_2(q)\in\partial H^n$ by Step A; hence $G(z)=T_{c_2}(\pi(\varphi_2(q)))=\psi_2(\psi_1^{-1}(z))$. So $G$ locally smoothly extends the boundary transition; the same construction applies to the inverse transition. Hence any two induced boundary charts are smoothly compatible. Their domains cover $\partial M$ (claim 3 applies to any boundary point and a chart of $M$ containing it), so they form a smooth atlas of dimension $n-1$; together with claim 2, $\partial M$ is a smooth manifold with boundary of dimension $n-1$. Since every chart image avoids $\partial H^{n-1}$ (claim 3), every point of $\partial M$ is an interior point in the sense of Interior Points, Boundary Points, and Boundary of a Smooth Manifold with Boundary, i.e. the boundary of $\partial M$ is empty.

Claim 5. $\partial M$ is closed in $M$ (claim 1) and $M$ is compact; by Closed Subset of a Compact Space is Compact, $\partial M$ is compact. $\blacksquare$