Theorems · Definition · algebraic topology

GenLoop.fromLoop

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

Generalized loop from a loop by uncurrying $I → (I^{N\setminus\{j\}} → X)$ into $I^N → X$.

Defined in

Mathlib.Topology.Homotopy.HomotopyGroup

Cited by

8 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceDecidableEq