In Professor Lee's Introduction to Smooth Manifolds (Second Edition), he states and proves Theorem 5.31, which guarantees that the smooth structure on an embedded or immersed submanifold of a smooth manifold is unique. A few pages later, he introduces smooth submanifolds with boundary and states and (sometimes) proves some theorems and propositions about them. But he gives no result for the uniqueness of the smooth structure of an embedded submanifold with boundary. I am wondering if there is a corresponding result (just for the embedded case).
I am particularly concerned about the case that arises in Theorem 9.25 (the Collar Neighborhood Theorem), whose proof creates a smooth embedding $$\phi\circ\psi\colon[0,1)\times\partial M\to M$$ whose image is an open subset of $M$. This smooth embedding is presumed to be a diffeomorphism (let's call it $E\colon[0,1)\times\partial M\to M$ and let's denote the image of $E$ by $C$) in the proofs of Theorem 9.26 and Theorem 9.29, which are the two theorems that can be used to show that a smooth manifold with boundary can be smoothly embedded in a smooth manifold (without boundary). As far as I can tell, the way to get $E$ to be a diffeomorphism is to appeal to a submanifold with boundary version of Proposition 5.18 (Images of Immersions as Submanifolds). Professor Lee doesn't offer exactly such a proposition, but I think I can prove the following extended version of Proposition 5.49(b):
Proposition 5.49(b'). Suppose $M$ is a smooth manifold with or without boundary. If $N$ is a smooth manifold with boundary and $F\colon N\to M$ is a smooth embedding, then with the subspace topology, $F(N)$ is a topological manifold with boundary, and it has a unique smooth structure making it into an embedded submanifold with boundary in $M$ with the property that $F$ is a diffeomorphism onto its image.
As with Proposition 5.18, this should be interpreted as saying that the smooth structure for $F(N)$ making $F$ a diffeomorphism onto $F(N)$ is unique, and with that smooth structure, $F(N)$ is an embedded submanifold of $M$.
But in working through the details of the proofs of Theorem 9.26 and Theorem 9.29, I haven't been able to prove some necessary smoothness claims using the smooth structure guaranteed by Proposition 5.49(b'). I have been careful not to make any uniqueness assumptions about the smooth structure $C$ has, other than $E$ is a diffeomorphism onto $C$. But $C$ is open in $M$ and therefore has a (possibly different) smooth structure as an open submanifold with boundary of $M$, with respect to which it is smoothly embedded in $M$. So if there were a uniqueness result of the kind I'm asking about, then the smooth structure for $C$ would be much easier to use to finish confirming the proofs of Theorem 9.26 and Theorem 9.29.
By the way, I contend that it would be circular to use the statement that one can lift the restriction that $M$ must have empty boundary in Theorem 5.53(b) and Theorem 5.29 (theorems about restricting the codomain of a smooth map to an embedded submanifold (with boundary)), when trying to prove Theorem 9.26 or Theorem 9.29, since I think that one or the other of them is needed to prove that restriction can be lifted.
I believe I have found a uniqueness result for the smooth structure in the case of an embedded submanifold with boundary.
The following theorem is an analogue of Theorem 5.31 (Uniqueness of Smooth Structures on Submanifolds) for embedded submanifolds with boundary. However it only claims that the smooth structure is unique once we assume the subspace topology, unlike Theorem 5.31 which also shows that the topology is unique even if we only assume the submanifold is immersed.
In fact, the topology is not unique for submanifolds with boundary, because for example the unit circle is an embedded submanifold with boundary in $\mathbb{R}^2$ (with empty boundary) but it is also an immersed submanifold with boundary with the topology given by the injective smooth immersion $\gamma: [0, 1) \to \mathbb{R}^2$ such that $\gamma(t) = (\cos 2\pi t, \sin 2\pi t)$. This makes it a submanifold with boundary where the boundary is $\{(1, 0)\}$, and there are open subsets containing $(1, 0)$ that are not open in the subspace topology, namely the images $\gamma([0, a))$ for $0 \lt a \lt 1$.
Since Theorem 5.51 is only stated for $M$ a smooth manifold without boundary, we cannot apply it in the case where $M$ itself has nonempty boundary.
Theorem
Suppose $M$ is a smooth manifold without boundary, and $S$ is an embedded submanifold with boundary. The smooth structure on $S$ described in Theorem 5.51 is the only smooth structure with respect to which $S$ is an embedded submanifold with boundary.
Proof
Most of the proof is copied verbatim from the proof of Theorem 5.31, with minor modifications to use the theorems for restricting the codomains of smooth maps between manifolds with boundary, and to exclude the possibility of a different topology. But we cannot use the Global Rank Theorem to show that $\widetilde{\iota}$ is a diffeomorphism. Instead, we show directly that it has a smooth inverse.
Suppose $S \subseteq M$ is an embedded $k$-dimensional submanifold with boundary. Theorem 5.51 shows that it satisfies the local $k$-slice condition for submanifolds with boundary, so it is an embedded submanifold with boundary with the subspace topology and the smooth structure of Theorem 5.51. Suppose there was some other smooth structure making it into an embedded submanifold with boundary. Let $\widetilde{S}$ denote the same set $S$, considered as a smooth manifold with boundary with the non-standard smooth structure, and let $\widetilde{\iota}: \widetilde{S} \hookrightarrow M$ denote the inclusion map, which by assumption is a smooth embedding. Because $\widetilde{\iota}(\widetilde{S}) = S$, Theorem 5.53 (b) implies that $\widetilde{\iota}$ is also smooth when considered as a map from $\widetilde{S}$ to $S$.
Since $\widetilde{S}$ is also an embedded submanifold with boundary, it also has the subspace topology. Therefore, $\widetilde{\iota}: \widetilde{S} \to S$ is a homeomorphism, so $\widetilde{\iota}^{-1}: S \to \widetilde{S}$ is continuous. It is the map obtained by restricting the codomain of the smooth map $\iota: S \hookrightarrow M$ to $\widetilde{S}$, which is an embedded submanifold with boundary in $M$. Therefore, Theorem 5.53 (b) also implies that $\widetilde{\iota}^{-1}: S \to \widetilde{S}$ is smooth.
These results show that $\widetilde{\iota}: \widetilde{S} \to S$ is a diffeomorphism and so $\widetilde{S}$ has the same smooth structure as $S$.