Theorems · Definition · algebraic topology

Path.Homotopy.hcomp

{X : Type u} →
  [inst : TopologicalSpace X] →
    {x₀ x₁ x₂ : X} →
      {p₀ q₀ : Path x₀ x₁} →
        {p₁ q₁ : Path x₁ x₂} → p₀.Homotopy q₀ → p₁.Homotopy q₁ → (p₀.trans p₁).Homotopy (q₀.trans q₁)

Suppose p₀ and q₀ are paths from x₀ to x₁, p₁ and q₁ are paths from x₁ to x₂. Furthermore, suppose F : Homotopy p₀ q₀ and G : Homotopy p₁ q₁. Then we can define a homotopy from p₀.trans p₁ to q₀.trans q₁.

Defined in

Mathlib.Topology.Homotopy.Path

Cited by

3 results in Mathlib

Foundations

Depth 129 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpace