Theorems · Definition · algebraic topology

Path.Homotopy.transAssoc

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

For paths p q r, we have a homotopy from (p.trans q).trans r to p.trans (q.trans r).

Defined in

Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpace