Finite-chart Euclidean embedding of a compact smooth manifold (source code)

= Finite-chart Euclidean embedding of a compact smooth manifold
{title2=$\Psi(x)=(\rho_i(x),\rho_i(x)\chi_i(x))_i$}

Choose finitely many coordinate charts on a <compact manifold> and smooth functions supported in them, positive on a cover. Extend the displayed chart products by zero. A positive first coordinate and its matching chart coordinates separate points, while their derivatives detect every nonzero tangent vector. Thus the map is an injective <immersion>; compactness makes it a <smooth embedding>. Extra zero coordinates make its codimension positive if required.