[proofplan] A point of $M$ is, by definition, a boundary point when some smooth chart sends it to the model boundary $\partial \mathbb{H}^k = \{x_k = 0\}$. The proof has two ingredients. First, we establish the **invariance of the boundary**: a diffeomorphism between open subsets of $\mathbb{H}^k$ cannot send an interior point to a boundary point, because the [Inverse Function Theorem](/page/Inverse%20Function%20Theorem) forces an interior point to have an open neighbourhood in $\mathbb{R}^k$ — a property that fails at boundary points. This makes "being a boundary point" a chart-independent property, so $\partial M$ is an intrinsically defined subset of $M$. Second, we restrict every boundary chart $(U,\varphi)$ of $M$ to $U \cap \partial M$. The restriction lands in $\partial \mathbb{H}^k \cong \mathbb{R}^{k-1}$, and the transition between two such restricted charts is the restriction of a smooth transition on $M$, hence smooth. The resulting atlas covers $\partial M$ and consists of charts into the *open* set $\mathbb{R}^{k-1}$, so $\partial M$ is a smooth $(k-1)$-manifold without boundary. [/proofplan]

[step:Fix the model half-space and recall the definition of a boundary chart] We work with the closed upper half-space and its topological pieces: \begin{align*} \mathbb{H}^k &:= \{x = (x_1,\ldots,x_k) \in \mathbb{R}^k : x_k \ge 0\}, \\ \partial \mathbb{H}^k &:= \{x \in \mathbb{H}^k : x_k = 0\}, \\ \operatorname{Int} \mathbb{H}^k &:= \{x \in \mathbb{H}^k : x_k > 0\}. \end{align*} A *chart* of $M$ is a pair $(U, \varphi)$ where $U \subseteq M$ is open and $\varphi: U \to V$ is a homeomorphism onto an [open set](/page/Open%20Set) $V \subseteq \mathbb{H}^k$. A function $F: V_1 \to V_2$ between open subsets of $\mathbb{H}^k$ is *smooth* if every point $x \in V_1$ admits an open neighbourhood $W \subseteq \mathbb{R}^k$ and a smooth extension $\tilde F: W \to \mathbb{R}^k$ with $\tilde F|_{W \cap V_1} = F|_{W \cap V_1}$. A *smooth atlas* on $M$ is a collection of charts whose domains cover $M$ and whose transition maps are smooth in this sense. The hypothesis is that $M$ carries such an atlas. A point $p \in M$ is a *boundary point* if there exists a chart $(U,\varphi)$ at $p$ with $\varphi(p) \in \partial \mathbb{H}^k$. Write $\partial M$ for the set of boundary points. [/step]

[step:Prove that diffeomorphisms of open subsets of $\mathbb{H}^k$ map interior to interior][claim:Invariance of the boundary] Let $V_1, V_2 \subseteq \mathbb{H}^k$ be open and let $F: V_1 \to V_2$ be a diffeomorphism (in the sense above). Then \begin{align*} F(V_1 \cap \operatorname{Int} \mathbb{H}^k) &\subseteq V_2 \cap \operatorname{Int} \mathbb{H}^k, \\ F(V_1 \cap \partial \mathbb{H}^k) &\subseteq V_2 \cap \partial \mathbb{H}^k. \end{align*} [/claim] [proof] Fix $p \in V_1 \cap \operatorname{Int} \mathbb{H}^k$. Since $V_1$ is open in $\mathbb{H}^k$ and $p$ lies in the (topological) interior of $\mathbb{H}^k$, there is an open ball $B(p, r) \subseteq V_1 \cap \operatorname{Int} \mathbb{H}^k$ for some $r > 0$, and $B(p,r)$ is open in $\mathbb{R}^k$. By smoothness, $F$ extends to a smooth map $\tilde F : W \to \mathbb{R}^k$ on some open neighbourhood $W \subseteq \mathbb{R}^k$ of $p$; shrinking $r$ if necessary, we may assume $B(p, r) \subseteq W$. Similarly the inverse $F^{-1}$ extends to a smooth map $\widetilde{F^{-1}}$ on some open neighbourhood $W' \subseteq \mathbb{R}^k$ of $F(p)$. Since $\tilde F$ is continuous at $p$ and $W'$ is open with $F(p) = \tilde F(p) \in W'$, choose $r' > 0$ with $B(p, r') \subseteq B(p, r)$ and $\tilde F(B(p, r')) \subseteq W'$. Then the composition $\widetilde{F^{-1}} \circ \tilde F$ is defined on $B(p, r')$ and agrees with the identity on $B(p, r') \cap \operatorname{Int} \mathbb{H}^k = B(p, r')$ since $B(p, r')$ already lies in the interior. Differentiating at $p$ and applying the [Chain Rule for Maps Between Euclidean Spaces](/theorems/323), we obtain \begin{align*} D(\widetilde{F^{-1}})_{F(p)} \circ D\tilde F_p = I_k, \end{align*} where $I_k$ is the identity on $\mathbb{R}^k$. Hence $D\tilde F_p$ is invertible. By the [Inverse Function Theorem](/theorems/51) applied to $\tilde F$ at $p$, there exist open sets $W_1 \subseteq \mathbb{R}^k$ around $p$ and $W_2 \subseteq \mathbb{R}^k$ around $F(p)$ such that $\tilde F: W_1 \to W_2$ is a diffeomorphism. Shrinking $W_1$ to lie inside $B(p, r')$, we have $W_1 \subseteq \operatorname{Int} \mathbb{H}^k$, so $\tilde F|_{W_1} = F|_{W_1}$. Therefore $F(p) \in W_2 \subseteq \mathbb{R}^k$ is contained in an open subset of $\mathbb{R}^k$ that is itself contained in $V_2 \subseteq \mathbb{H}^k$. This forces $W_2 \subseteq \operatorname{Int} \mathbb{H}^k$: if $z \in W_2 \cap \partial \mathbb{H}^k$, then because $W_2$ is open in $\mathbb{R}^k$, some Euclidean ball $B(z,\rho)$ with $\rho > 0$ lies in $W_2$; but $B(z,\rho)$ contains points with negative $k$-th coordinate, contradicting $W_2 \subseteq \mathbb{H}^k$. In particular $F(p) \in \operatorname{Int} \mathbb{H}^k$. This proves $F(V_1 \cap \operatorname{Int} \mathbb{H}^k) \subseteq V_2 \cap \operatorname{Int} \mathbb{H}^k$. Applying the identical argument to $F^{-1}: V_2 \to V_1$ gives the reverse inclusion $F^{-1}(V_2 \cap \operatorname{Int} \mathbb{H}^k) \subseteq V_1 \cap \operatorname{Int} \mathbb{H}^k$, i.e.\ $F$ maps interior bijectively to interior. The complementary statement on boundaries follows because $V_1 = (V_1 \cap \operatorname{Int} \mathbb{H}^k) \sqcup (V_1 \cap \partial \mathbb{H}^k)$ and similarly for $V_2$. [/proof][/step]

[guided]We want to show that a diffeomorphism between open subsets of the half-space cannot accidentally turn an interior point into a boundary point. The intuition is purely topological: an interior point $p \in \operatorname{Int} \mathbb{H}^k$ has an *honest* open neighbourhood in $\mathbb{R}^k$ inside $V_1$; the diffeomorphism, being smooth with smooth inverse, should preserve this local Euclidean structure. The [Inverse Function Theorem](/theorems/51) makes this rigorous. Fix $p \in V_1 \cap \operatorname{Int} \mathbb{H}^k$. Two facts about $p$: (i) since $V_1$ is open in $\mathbb{H}^k$ and $p$ is already in the $\mathbb{R}^k$-interior of $\mathbb{H}^k$, every sufficiently small ball $B(p,r)$ lies in $V_1$, and this ball is open in $\mathbb{R}^k$; (ii) by hypothesis $F$ admits a smooth extension $\tilde F$ to an open neighbourhood $W \subseteq \mathbb{R}^k$ of $p$, and $F^{-1}$ admits an extension $\widetilde{F^{-1}}$ near $F(p)$. Why is $D\tilde F_p$ invertible? On the open Euclidean ball $B(p, r') \subseteq V_1 \cap \operatorname{Int}\mathbb{H}^k$ (with $r'$ small enough so both extensions are defined), we have $\widetilde{F^{-1}} \circ \tilde F = \operatorname{id}$ on a *full Euclidean [open set](/page/Open%20Set)*, not just on a one-sided piece. Differentiating at $p$ using the [Chain Rule for Maps Between Euclidean Spaces](/theorems/323) gives $D(\widetilde{F^{-1}})_{F(p)} \circ D\tilde F_p = I_k$, so $D\tilde F_p$ is invertible. Now apply the [Inverse Function Theorem](/theorems/51) to $\tilde F$ at $p$: there are open sets $W_1 \subseteq \mathbb{R}^k$ around $p$ and $W_2 \subseteq \mathbb{R}^k$ around $F(p)$ with $\tilde F: W_1 \to W_2$ a diffeomorphism. We shrink $W_1$ to fit inside $B(p, r') \subseteq \operatorname{Int}\mathbb{H}^k$. On this $W_1$, $\tilde F = F$, so $F(p) \in W_2$ where $W_2$ is open in $\mathbb{R}^k$ and contained in $V_2 \subseteq \mathbb{H}^k$. Why does this force $F(p) \in \operatorname{Int}\mathbb{H}^k$? Because $\partial \mathbb{H}^k$ has empty interior in $\mathbb{R}^k$ — no open ball of $\mathbb{R}^k$ fits inside the hyperplane $\{x_k = 0\}$. So any open subset of $\mathbb{R}^k$ that lies inside $\mathbb{H}^k$ must miss $\partial \mathbb{H}^k$ entirely, i.e.\ be contained in $\operatorname{Int} \mathbb{H}^k$. Hence $F(p) \in W_2 \subseteq \operatorname{Int} \mathbb{H}^k$. This shows $F$ sends $V_1$-interior into $V_2$-interior. Applying the same argument to the smooth inverse $F^{-1}$ shows it sends $V_2$-interior into $V_1$-interior; combined, $F$ restricts to a bijection of interiors. Then the boundary pieces $V_1 \cap \partial \mathbb{H}^k$ and $V_2 \cap \partial \mathbb{H}^k$ — the set-theoretic complements within $V_1$ and $V_2$ — must also be in bijection under $F$.[/guided]

[step:Conclude that being a boundary point is chart-independent] Suppose $p \in M$ and $(U_1, \varphi_1)$, $(U_2, \varphi_2)$ are two charts of $M$ at $p$. The transition map \begin{align*} \tau := \varphi_2 \circ \varphi_1^{-1} : \varphi_1(U_1 \cap U_2) \longrightarrow \varphi_2(U_1 \cap U_2) \end{align*} is a diffeomorphism between open subsets of $\mathbb{H}^k$ (smooth atlas hypothesis on $M$). By the invariance of the boundary established above, $\tau$ maps $\partial \mathbb{H}^k$-points to $\partial \mathbb{H}^k$-points and $\operatorname{Int} \mathbb{H}^k$-points to $\operatorname{Int} \mathbb{H}^k$-points. Since $\tau(\varphi_1(p)) = \varphi_2(p)$, we conclude \begin{align*} \varphi_1(p) \in \partial \mathbb{H}^k \iff \varphi_2(p) \in \partial \mathbb{H}^k. \end{align*} Therefore the condition "$\varphi(p) \in \partial \mathbb{H}^k$ for some chart $(U,\varphi)$ at $p$" is equivalent to "$\varphi(p) \in \partial \mathbb{H}^k$ for every chart at $p$." The set $\partial M$ is intrinsically defined, and its complement $M \setminus \partial M$ consists of those $p$ with $\varphi(p) \in \operatorname{Int} \mathbb{H}^k$ in every (equivalently, some) chart. [/step]

[step:Construct an atlas on $\partial M$ by restricting boundary charts] Identify $\partial \mathbb{H}^k$ with $\mathbb{R}^{k-1}$ via the canonical projection map \begin{align*} \pi : \partial \mathbb{H}^k &\to \mathbb{R}^{k-1} \\ (x_1, \ldots, x_{k-1}, 0) &\mapsto (x_1, \ldots, x_{k-1}), \end{align*} which is a homeomorphism. For any chart $(U, \varphi)$ of $M$ with $U \cap \partial M \ne \varnothing$, define the *boundary chart restriction* \begin{align*} \varphi^\partial : U \cap \partial M &\to \pi(\varphi(U) \cap \partial \mathbb{H}^k) \subseteq \mathbb{R}^{k-1} \\ p &\mapsto \pi(\varphi(p)). \end{align*} We verify the four conditions required of a chart on $\partial M$. **(a) Domain is open in $\partial M$.** Since $U$ is open in $M$ and $\partial M$ carries the [subspace topology](/page/Subspace%20Topology), $U \cap \partial M$ is open in $\partial M$. **(b) Codomain is open in $\mathbb{R}^{k-1}$.** The set $\varphi(U) \subseteq \mathbb{H}^k$ is open in $\mathbb{H}^k$, so $\varphi(U) \cap \partial \mathbb{H}^k$ is open in $\partial \mathbb{H}^k$, and $\pi$ is a homeomorphism. Hence $\pi(\varphi(U) \cap \partial \mathbb{H}^k)$ is open in $\mathbb{R}^{k-1}$. **(c) $\varphi^\partial$ is a homeomorphism onto its image.** It is the composition $\pi \circ (\varphi|_{U \cap \partial M})$ of two homeomorphisms onto their images: the restriction of $\varphi$ to the closed subset $U \cap \partial M = \varphi^{-1}(\varphi(U) \cap \partial \mathbb{H}^k)$, followed by $\pi$. Both maps are continuous bijections with continuous inverses on their respective images. **(d) The collection of all such $\varphi^\partial$ covers $\partial M$.** By definition every $p \in \partial M$ lies in some boundary chart $(U,\varphi)$ of $M$, and $p \in U \cap \partial M$ is then in the domain of $\varphi^\partial$. [/step]

[step:Verify smoothness of transitions between restricted charts] Let $(U_1, \varphi_1)$ and $(U_2, \varphi_2)$ be boundary charts of $M$ with $U_1 \cap U_2 \cap \partial M \ne \varnothing$. The transition between the restricted charts is \begin{align*} \varphi_2^\partial \circ (\varphi_1^\partial)^{-1} : \pi(\varphi_1(U_1 \cap U_2) \cap \partial \mathbb{H}^k) \longrightarrow \pi(\varphi_2(U_1 \cap U_2) \cap \partial \mathbb{H}^k). \end{align*} Unpacking the definitions, this is the composition \begin{align*} y \;\xmapsto{\pi^{-1}}\; (y, 0) \;\xmapsto{\tau}\; \tau(y, 0) \;\xmapsto{\pi}\; \pi(\tau(y, 0)), \end{align*} where $\tau = \varphi_2 \circ \varphi_1^{-1}$ is the full transition map on $M$. By the invariance of the boundary applied to $\tau$, the image $\tau(y, 0)$ lies in $\partial \mathbb{H}^k$, so the final projection $\pi$ is well-defined. Thus \begin{align*} \bigl(\varphi_2^\partial \circ (\varphi_1^\partial)^{-1}\bigr)(y) &= (\tau_1(y, 0), \ldots, \tau_{k-1}(y, 0)), \end{align*} where $\tau = (\tau_1, \ldots, \tau_k)$ are the component functions of $\tau$. Each $\tau_i$ is smooth on an open neighbourhood of every point $(y, 0)$ in the sense of §1 (extending to a smooth function on an open subset of $\mathbb{R}^k$). Restricting to the hyperplane $\{x_k = 0\}$ — that is, plugging in $x_k = 0$ — yields a smooth function of $y \in \mathbb{R}^{k-1}$ on the corresponding open subset (the restriction of a smooth function on an open subset of $\mathbb{R}^k$ to an affine subspace is smooth, by composition with the smooth inclusion $y \mapsto (y, 0)$ and the [Chain Rule for Maps Between Euclidean Spaces](/theorems/323)). Hence each component of $\varphi_2^\partial \circ (\varphi_1^\partial)^{-1}$ is smooth, and so is the transition map. The restricted charts therefore form a smooth atlas on $\partial M$. [/step]

[step:Show that $\partial M$ has no boundary and has dimension $k-1$] The hypothesis $k \ge 1$ ensures that $k-1$ is a non-negative integer, so $\mathbb{R}^{k-1}$ is a valid Euclidean model space. The charts $\varphi^\partial$ constructed in the previous steps map open subsets of $\partial M$ homeomorphically onto open subsets of the full Euclidean space $\mathbb{R}^{k-1}$. This is exactly the local model for a smooth manifold without boundary of dimension $k - 1$. Since every $\varphi^\partial$ takes values in an open subset of $\mathbb{R}^{k-1}$, the resulting smooth structure has no boundary points. Explicitly: for any $q \in \partial M$ and any restricted chart $\varphi^\partial$ at $q$, the image $\varphi^\partial(q) \in \mathbb{R}^{k-1}$ lies in the open subset $\pi(\varphi(U) \cap \partial \mathbb{H}^k) \subseteq \mathbb{R}^{k-1}$. There is no "boundary of $\mathbb{R}^{k-1}$" — the model space of $\partial M$'s charts is the full $\mathbb{R}^{k-1}$. Therefore $\partial(\partial M) = \varnothing$. Combining the previous steps: the collection $\{(U \cap \partial M, \varphi^\partial)\}$ ranging over boundary charts $(U, \varphi)$ of $M$ is a smooth atlas on $\partial M$ into $\mathbb{R}^{k-1}$ with no boundary charts, exhibiting $\partial M$ as a smooth $(k-1)$-dimensional manifold without boundary. This completes the proof. [/step]