Theorems · Theorem · algebraic topology

GenLoop.currySum_apply_inl_inr

∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {M : Type u_3} (x : X) (p : ↑(GenLoop (M ⊕ N) X x))
  (y : M ⊕ N → ↑unitInterval), ((GenLoop.currySum x p) (y ∘ Sum.inl)) (y ∘ Sum.inr) = p y

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