OAI/Topology/Homotopy/LoopHomotopy.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Loop-space homeomorphisms and the degree-shift equivalence.

  1. theorem OAI.NearbyLagrangian.BasedHomotopy.genLoop_homotopic_iff_joined line 17
  2. def OAI.NearbyLagrangian.BasedHomotopy.piEquivOfLoopHomeomorph line 42
  3. def OAI.NearbyLagrangian.BasedHomotopy.piReindexEquiv line 53
  4. def OAI.NearbyLagrangian.BasedHomotopy.flattenPathLoop line 57
  5. def OAI.NearbyLagrangian.BasedHomotopy.curryPathLoop line 72
  6. lemma OAI.NearbyLagrangian.BasedHomotopy.curry_flatten line 86
  7. lemma OAI.NearbyLagrangian.BasedHomotopy.flatten_curry line 92
  8. lemma OAI.NearbyLagrangian.BasedHomotopy.continuous_flattenPathLoop line 103
  9. lemma OAI.NearbyLagrangian.BasedHomotopy.continuous_curryPathLoop line 114
  10. def OAI.NearbyLagrangian.BasedHomotopy.loopSpaceCubeHomeomorph line 121
  11. def OAI.NearbyLagrangian.BasedHomotopy.loopPiEquiv line 130
  12. def OAI.NearbyLagrangian.BasedHomotopy.pi9LoopEquivPi10 line 134