English
A path Γ equals liftPath γ e γ0 if and only if p ∘ Γ = γ and Γ(0)=e, together with continuity of Γ.
Русский
Путь Γ равен liftPath γ e γ0 тогда и только тогда, когда p ∘ Γ = γ и Γ(0)=e совместно с непрерывностью Γ.
LaTeX
$$$$\Gamma = \text{liftPath}(\gamma,e,\gamma_0) \iff (p \circ \Gamma = \gamma) \land (\Gamma(0)=e) \land \text{Continuous}(\Gamma).$$$$
Lean4
theorem eq_liftPath_iff {Γ : I → E} : Γ = cov.liftPath γ e γ_0 ↔ Continuous Γ ∧ p ∘ Γ = γ ∧ Γ 0 = e :=
have lifts := cov.liftPath_lifts γ e γ_0
have zero := cov.liftPath_zero γ e γ_0
⟨(· ▸ ⟨(cov.liftPath γ e γ_0).2, lifts, zero⟩), fun ⟨Γ_cont, Γ_lifts, Γ_0⟩ ↦
cov.eq_of_comp_eq Γ_cont (cov.liftPath γ e γ_0).continuous (Γ_lifts ▸ lifts.symm) 0 (Γ_0 ▸ zero.symm)⟩
