Theorems · Definition · algebraic topology

GenLoop.currySum

{N : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace X] →
      {M : Type u_3} → (x : X) → ↑(GenLoop (M ⊕ N) X x) → C(M → ↑unitInterval, ↑(GenLoop N X x))

Curries an (M ⊕ N)-cube into an M-cube of N-cubes.

Defined in

Mathlib.Topology.Homotopy.HomotopyGroup

Cited by

4 results in Mathlib

Foundations

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

Assumes

TopologicalSpace