liftHomotopy_lifts

Mathlib.Topology.Homotopy.Lifting

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

English

The lifted homotopy Γ lifts H: p ∘ Γ = H, and Γ_0 corresponds to f via H_0, i.e., Γ_0 is lifted from f.

Русский

Подъём гомотопии Γ поднимает H: p ∘ Γ = H, а Γ_0 соответствует f через H_0.

LaTeX

$$$$p \circ cov.liftHomotopy(H,f,H_0) = H,$$$$

Lean4

theorem liftHomotopy_lifts : p ∘ cov.liftHomotopy H f H_0 = H :=
  funext fun ⟨t, _⟩ ↦ congr_fun (cov.liftPath_lifts ..) t

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

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

Разделы

Аффилиация

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