hcomp — Mathlib

English

If F : p0.Homotopy p1 and G : p1.Homotopy p2, then F.hcomp G is a Homotopy from p0.trans p1 to p1.trans p2.

Русский

Если F : p0.Homotopy p1 и G : p1.Homotopy p2, то F.hcomp G — гомотопия от p0.trans p1 к p1.trans p2.

LaTeX

$$$\forall F : p_0.Homotopy p_1,\; G : p_1.Homotopy p_2,\; (F.hcomp G) : (p_0.trans p_1).Homotopy (p_1.trans p_2)$$$

Lean4

theorem hcomp {p₀ p₁ : Path x₀ x₁} {q₀ q₁ : Path x₁ x₂} (hp : p₀.Homotopic p₁) (hq : q₀.Homotopic q₁) :
    (p₀.trans q₀).Homotopic (p₁.trans q₁) :=
  hp.map2 Homotopy.hcomp hq

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