 Regular level set theorem

The preimage of a regular value of a smooth map between manifolds is a smooth submanifold whose codimension equals the dimension of the target.