Theorems · Definition · algebraic topology

GenLoop.toLoop

{N : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace X] →
      {x : X} → [DecidableEq N] → (i : N) → ↑(GenLoop N X x) → LoopSpace (↑(GenLoop { j // j ≠ i } X x)) GenLoop.const

Loop from a generalized loop by currying $I^N → X$ into $I → (I^{N\setminus\{j\}} → X)$.

Defined in

Mathlib.Topology.Homotopy.HomotopyGroup

Cited by

12 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceDecidableEq