liftPath_lifts

Mathlib.Topology.Homotopy.Lifting

URI: https://scilib.ai/kg/mathlib#IsCoveringMap.liftPath_lifts

English

The lifted path satisfies p ∘ liftPath γ e γ0 = γ.

Русский

Подъём пути удовлетворяет p ∘ liftPath γ e γ0 = γ.

LaTeX

$$$$p \circ \text{liftPath}(\gamma,e,\gamma_0) = \gamma.$$$$

Lean4

theorem liftPath_lifts : p ∘ cov.liftPath γ e γ_0 = γ :=
  (cov.exists_path_lifts γ e γ_0).choose_spec.1

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru