The Euclidean tubular neighbourhood theorem

If $S=\mathrm{\varnothing }$, take the unique function $\delta :S\to (0,\mathrm{\infty })$. Then ${\mathrm{\Omega }}_{\delta }=\mathrm{\varnothing }$, and $E$ is a diffeomorphism from the empty manifold onto the open neighbourhood $\mathrm{\varnothing }$ of $S$. Hence assume $S\mathrm{\ne }\mathrm{\varnothing }$.

Let $W$ be the union of all normal-bundle neighbourhoods on which [L2] makes $E$ a local diffeomorphism. It is open and contains the zero section. By shrinking bundle trivializations around their base points, choose an open cover $(U_i)$ of $S$ and numbers $r_i>0$ such that $\{(p,v):p\in U_i,\mathrm{\parallel }v\mathrm{\parallel }<r_i\}\subseteq W\mathrm{.}$ By [L3], choose a locally finite smooth partition $({\varphi }_i)$ subordinate to this cover.

Define $r(p):={\left({\sum }_i\frac{{\varphi }_i(p)}{r_i}\right)}^{-1}\mathrm{.}$ The locally finite sum is smooth and positive. At each $p$, the finite nonempty set $I(p):=\{i:{\varphi }_i(p)>0\}$ has an index $i_0$ with $r_{i_0}={\max }_{i\in I(p)}{r}_i$. Since $r(p)\le r_{i_0}$ and $p\in \mathrm{supp}({\varphi }_{i_0})\subseteq U_{i_0}$, the whole fibre ball $\mathrm{\parallel }v\mathrm{\parallel }<r(p)$ over $p$ lies in $W$.

Let ${\delta }_0:S\to (0,\mathrm{\infty })$ be the positive smooth injectivity radius supplied by [L2], and put $\delta (p):=\frac{{\delta }_0(p)r(p)}{{\delta }_0(p)+r(p)}\mathrm{.}$ This function is positive and smooth, with $\delta <{\delta }_0$ and $\delta <r$.

The set ${\mathrm{\Omega }}_{\delta }$ is open in $N^{\perp }S$ because $(p,v)\mapsto \mathrm{\parallel }v\mathrm{\parallel }-\delta (p)$ is continuous. Since $\delta <r$, step 3.1 gives ${\mathrm{\Omega }}_{\delta }\subseteq W$, so $E$ is a local diffeomorphism at every point of ${\mathrm{\Omega }}_{\delta }$. Since $\delta <{\delta }_0$, [L2] also makes $E$ injective on ${\mathrm{\Omega }}_{\delta }$.

A local diffeomorphism is open. Hence $U:=E({\mathrm{\Omega }}_{\delta })$ is open and contains $S$ because $E(p,0)=p$. The injective local diffeomorphism $E:{\mathrm{\Omega }}_{\delta }\to U$ is a homeomorphism, and its local smooth inverses agree and assemble to a smooth global inverse. Thus $E$ is the required diffeomorphism. Together with the empty case in step 1.1, this proves the theorem.