Theorems · Theorem · algebraic topology

GenLoop.homotopyFrom_apply

∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} [inst_1 : DecidableEq N] (i : N)
  {p q : ↑(GenLoop N X x)} (H : Path.Homotopy (GenLoop.toLoop i p) (GenLoop.toLoop i q))
  (a : ↑unitInterval × (N → ↑unitInterval)),
  (GenLoop.homotopyFrom i H) a =
    Function.uncurry (fun x_1 y => Function.uncurry (fun x_2 y => (H (x_1, x_2)) y) y)
      (Prod.map id (⇑(Cube.splitAt i)) a)

Defined in

Mathlib.Topology.Homotopy.HomotopyGroup

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceDecidableEq