Homotopy lifting theorem for a covering map (source code)

= Homotopy lifting theorem for a covering map

= Homotopy lifting lemma
{synonym}

A homotopy into the base of a <covering space> has a unique continuous lift once its initial map is continuously lifted. Local inverse sheets construct the lift along each time interval, and compactness of that interval permits a finite subdivision locally around each point of the homotopy's parameter space. Uniqueness on overlapping intervals follows from <path lifting theorem> uniqueness. In a homotopy of paths with endpoints fixed, a chosen lifted endpoint remains fixed because it varies continuously in a discrete fiber.