path lifting property

《Algebraic Topology》 · 第 60 页 · Proposition 1.30

For a covering map \(p:\widetilde X\to X\), each path \(f:I\to X\) and each \(\widetilde x_0\in p^{-1}(f(0))\) have a unique lifted path \(\widetilde f:I\to\widetilde X\) starting at \(\widetilde x_0\).