liftPath_zero

Mathlib.Topology.Homotopy.Lifting

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

English

At the initial time, the lifted path starts at the given base point: liftPath γ e γ0 (0) = e.

Русский

В начальный момент подъём стартует в заданной точке: liftPath γ e γ0 (0) = e.

LaTeX

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

Lean4

theorem liftPath_zero : cov.liftPath γ e γ_0 0 = e :=
  (cov.exists_path_lifts γ e γ_0).choose_spec.2

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

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

Разделы

Аффилиация

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