OAI/Topology/Homotopy/BasedMaps.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Maps of based generalized loops and homotopy groups.

  1. def OAI.NearbyLagrangian.BasedHomotopy.loopMap line 16
  2. lemma OAI.NearbyLagrangian.BasedHomotopy.loopMap_homotopic line 19
  3. theorem OAI.NearbyLagrangian.BasedHomotopy.loopMap_const line 24
  4. theorem OAI.NearbyLagrangian.BasedHomotopy.loopMap_id line 27
  5. theorem OAI.NearbyLagrangian.BasedHomotopy.loopMap_comp line 30
  6. lemma OAI.NearbyLagrangian.BasedHomotopy.loopMap_transAt line 35
  7. def OAI.NearbyLagrangian.BasedHomotopy.groupMap line 42
  8. theorem OAI.NearbyLagrangian.BasedHomotopy.groupMap_id line 56
  9. theorem OAI.NearbyLagrangian.BasedHomotopy.groupMap_comp line 61