covering homotopy theorem

《一般拓扑学基础》 · 第 277–278 页 · Theorem 10.5

Let \(p:\widetilde X\to X\) be a covering map, \(F:Y\times I\to X\) a homotopy, and \(\widetilde f:Y\to\widetilde X\) a lift of \(F|_{Y\times\{0\}}\). If \(Y\) is connected, there is a unique lift \(\widetilde F:Y\times I\to\widetilde X\) extending \(\widetilde f\).