Theorems · Definition · algebraic topology

GenLoop.homotopyFrom

{N : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace X] →
      {x : X} →
        [inst_1 : DecidableEq N] →
          (i : N) →
            {p q : ↑(GenLoop N X x)} →
              Path.Homotopy (GenLoop.toLoop i p) (GenLoop.toLoop i q) → C(↑unitInterval × (N → ↑unitInterval), X)

The converse to GenLoop.homotopyTo: a homotopy between two loops in the space of n-dimensional loops can be seen as a homotopy between two n+1-dimensional paths.

Defined in

Mathlib.Topology.Homotopy.HomotopyGroup

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceDecidableEq