English
If γ0 and γ1 are homotopic rel {0,1}, then the endpoints of their lifts through a covering map from a fixed base e coincide: liftPath γ0 e γ0(0) at 1 equals liftPath γ1 e γ1(0) at 1.
Русский
Если γ0 и γ1 гомотопны относительно {0,1}, концы подъёмов через покрывающую карту совпадают: liftPath γ0 e γ0(0) 1 = liftPath γ1 e γ1(0) 1.
LaTeX
$$$$\text{liftPath }(\gamma_0, e, \gamma_0(0)) (1) = \text{liftPath }(\gamma_1, e, \gamma_1(0)) (1).$$$$
Lean4
/-- Lifting two paths that are homotopic relative to {0,1}
starting from the same point also ends up in the same point. -/
theorem liftPath_apply_one_eq_of_homotopicRel {γ₀ γ₁ : C(I, X)} (h : γ₀.HomotopicRel γ₁ {0, 1}) (e : E)
(h₀ : γ₀ 0 = p e) (h₁ : γ₁ 0 = p e) : cov.liftPath γ₀ e h₀ 1 = cov.liftPath γ₁ e h₁ 1 :=
by
obtain ⟨H⟩ := h
have :=
cov.liftHomotopyRel (f₀' := cov.liftPath γ₀ e h₀) (f₁' := cov.liftPath γ₁ e h₁) H
⟨0, .inl rfl, by simp_rw [liftPath_zero]⟩ (liftPath_lifts ..) (liftPath_lifts ..)
rw [← this.eq_fst 0 (.inr rfl), ← this.eq_snd 0 (.inr rfl)]
