OAI/GroupTheory/FiniteType/HomotopyFunctor.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HomotopyFunctor.loopMap line 23
  2. theorem OAI.HomotopyFunctor.loopMap_apply line 26
  3. theorem OAI.HomotopyFunctor.loopMap_homotopic line 29
  4. def OAI.HomotopyFunctor.map line 33
  5. theorem OAI.HomotopyFunctor.map_mk line 36
  6. theorem OAI.HomotopyFunctor.map_id line 39
  7. theorem OAI.HomotopyFunctor.map_comp line 43
  8. theorem OAI.HomotopyFunctor.loopMap_transAt line 51
  9. def OAI.HomotopyFunctor.mapHom line 61
  10. theorem OAI.HomotopyFunctor.mapHom_eq_of_homotopy line 78
  11. def OAI.HomotopyFunctor.equiv line 97
  12. def OAI.HurewiczConstruction.sphereData line 125
  13. theorem OAI.HurewiczConstruction.sphereData_boundary line 129
  14. theorem OAI.HurewiczConstruction.sphereData_factors line 133
  15. def OAI.HurewiczConstruction.sphereMap line 149
  16. theorem OAI.HurewiczConstruction.sphereMap_apply_quot line 152
  17. theorem OAI.HurewiczConstruction.sphereMap_pole line 156
  18. def OAI.HurewiczConstruction.homotopyData line 159
  19. theorem OAI.HurewiczConstruction.homotopyData_boundary line 167
  20. theorem OAI.HurewiczConstruction.homotopyData_factors line 173
  21. def OAI.HurewiczConstruction.sphereHomotopy line 190
  22. abbrev OAI.HurewiczConstruction.integralHomology line 212
  23. def OAI.HurewiczConstruction.pushforward line 215
  24. theorem OAI.HurewiczConstruction.pushforward_homotopic line 218
  25. def OAI.HurewiczConstruction.map line 224
  26. theorem OAI.HurewiczConstruction.map_mk line 230
  27. theorem OAI.HurewiczConstruction.pushforward_comp line 233
  28. theorem OAI.HurewiczConstruction.sphereMap_natural line 239
  29. theorem OAI.HurewiczConstruction.map_natural line 250
  30. theorem OAI.HurewiczConstruction.pushforward_const line 257
  31. theorem OAI.HurewiczConstruction.sphereMap_const line 270
  32. theorem OAI.HurewiczConstruction.map_one line 277