liftHomotopy_zero — Mathlib

English

lifting a homotopy Rel S of two maps f0, f1 through a covering map p given a lifting of endpoints on S yields a lifted homotopy Rel S.

Русский

Подъём гомотопии относительно множества S двух отображений f0, f1 через покрывающую карту p даёт подъём гомотопии Rel S.

LaTeX

$$$$\text{liftHomotopyRel} : f_0.HomotopyRel f_1 S \to \text{(lifted object)}.$$$$

Lean4

theorem liftHomotopy_zero (a : A) : cov.liftHomotopy H f H_0 (0, a) = f a :=
  cov.liftPath_zero ..

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