Theorems · Theorem · algebraic topology

GenLoop.currySum_apply_coe

∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {M : Type u_3} (x : X) (q : ↑(GenLoop (M ⊕ N) X x))
  (a : M → ↑unitInterval),
  ↑((GenLoop.currySum x q) a) =
    ((↑q).comp { toFun := Homeomorph.sumArrowHomeomorphProdArrow.invFun, continuous_toFun := ⋯ }).curry.toFun a

Defined in

Mathlib.Topology.Homotopy.HomotopyGroup

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpace