Tubular neighborhood theorem (source code)

= Tubular neighborhood theorem

A smooth embedded <submanifold> has a neighborhood diffeomorphic to a neighborhood of the <zero section> of its <normal bundle>, with the <zero section> identified with the <submanifold>. One may prescribe the normal-bundle splitting of the derivative along that section. Choose a <Riemannian metric> making the splitting orthogonal and use its normal exponential map: its derivative there is the required <isomorphism>, so the <inverse function theorem> supplies local <diffeomorphisms>. A sufficiently small, possibly varying, fibre radius makes these fit into a <tubular neighborhood>.