liftPath — Mathlib

English

A liftPath is the lifted path to the covering space corresponding to a given γ and initial data; it’s defined as lift of γ to E starting at e.

Русский

LiftPath — подъём пути в пространство покрытия, соответствующий γ и начальному значению e.

LaTeX

$$$$\text{liftPath }:\; \text{IsCoveringMap } p \to (\gamma: C(I,X)) \to (e:E) \to C(I,E).$$$$

Lean4

/-- The lift of a path to a covering space given a lift of the left endpoint. -/
noncomputable def liftPath : C(I, E) :=
  (cov.exists_path_lifts γ e γ_0).choose

Похожие утверждения