Definition (boundary):
Let be a differentiable manifold equipped with an atlas . Further, let be the set of all such that maps to an open subset of the half-space equipped with its subspace topology w.r.t. . The boundary of , commonly denoted by , is defined as follows:
Proposition (the boundary of a differentiable manifold with boundary is a differentiable manifold):
Let be a differentiable manifold with boundary of class and let be an atlas of . Then is a differentiable manifold with boundary of class , and the family
constitutes an atlas of , where is defined as follows:
Proof: First, we prove that for each , the function is a homeomorphism.
To this end, it is prudent to observe that whenever and such that contains (where shall denote the domain of definition of ), then . This is because by the definition of , there exists a and an such that
- ;
yet the function is a homeomorphism, whence so is its inverse, so that upon assuming that , the closedness of the latter set permits the choice of an open neighbourhood of that does not intersect , and Brouwer's invariance of domain theorem then implies that
is an open neighbourhood of with respect to the Euclidean topology of , whereas the same set must be contained within the image of , which is in turn contained within , so that cannot intersect , for otherwise it would contain one of its boundary points and hence be not closed, contradicting the assumption that .
This proves that whenever , the function maps to . Hence, when restricted to the image of , the function is invertible and in fact a homeomorphism between a subset of endowed with its subspace topology and . In fact, restricted in this way, is a diffeomorphism of class .
Moreover, is a homeomorphism since the restriction of a homeomorphism is again a homeomorphism. Hence,
is a homeomorphism as the composition of homeomorphisms; indeed, is a homeomorphism between a subset of and a subset of .
Let now . Then
- ,
and the differentiability condition now follows from the fact that the composition of the three functions , and [[is times differentiable as the composition of times differentiable functions]].
Finally, by the very definition of the domains of definition of the functions in the family cover all of .