OAI/GroupTheory/FiniteType/SingularSphereCycle.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SingularSphereCycle.collapse line 25
  2. lemma OAI.SingularSphereCycle.face_zero line 28
  3. lemma OAI.SingularSphereCycle.collapse_face line 32
  4. def OAI.SingularSphereCycle.simplex line 38
  5. lemma OAI.SingularSphereCycle.simplex_face line 42
  6. abbrev OAI.SingularSphereCycle.chains line 48
  7. def OAI.SingularSphereCycle.cycle line 51
  8. lemma OAI.SingularSphereCycle.cycle_d_succ line 56
  9. lemma OAI.SingularSphereCycle.cycle_d line 69
  10. def OAI.SingularSphereCycle.fundamentalClass line 74
  11. def OAI.HurewiczConstruction.canonical line 85
  12. theorem OAI.HurewiczConstruction.canonical_mk line 88
  13. theorem OAI.HurewiczConstruction.canonical_natural line 91
  14. theorem OAI.HurewiczConstruction.canonical_one line 96
  15. abbrev OAI.BasedSimplex.Std line 107
  16. def OAI.BasedSimplex.Boundary line 108
  17. def OAI.BasedSimplex.Space line 110
  18. instance OAI.BasedSimplex.(instance at line 113) line 113
  19. theorem OAI.BasedSimplex.ext line 117
  20. def OAI.BasedSimplex.cubeEquiv line 120
  21. lemma OAI.BasedSimplex.cubeEquiv_boundary line 123
  22. def OAI.BasedSimplex.loop line 133
  23. def OAI.BasedSimplex.ofLoop line 137
  24. lemma OAI.BasedSimplex.loop_ofLoop line 141
  25. lemma OAI.BasedSimplex.ofLoop_loop line 146
  26. def OAI.BasedSimplex.homotopyClass line 151
  27. def OAI.BasedSimplex.const line 153
  28. lemma OAI.BasedSimplex.loop_const line 155
  29. lemma OAI.BasedSimplex.class_const line 157
  30. def OAI.BasedSimplex.map line 160
  31. lemma OAI.BasedSimplex.class_homotopic line 164
  32. def OAI.BasedSimplex.homotopy_of_loop line 179
  33. lemma OAI.BasedSimplex.class_eq_iff line 205
  34. def OAI.HurewiczNormalized.cycle line 222
  35. lemma OAI.HurewiczNormalized.based_face line 225
  36. lemma OAI.HurewiczNormalized.cycle_d line 230
  37. def OAI.HurewiczNormalized.cycleClassHom line 242
  38. lemma OAI.HurewiczNormalized.cycleClassHom_map line 249
  39. def OAI.HurewiczNormalized.homologyClass line 257
  40. lemma OAI.HurewiczNormalized.sphereMap_comp_collapse line 260
  41. lemma OAI.HurewiczNormalized.sphereCycle_map line 271
  42. theorem OAI.HurewiczNormalized.canonical_simplex line 282
  43. def OAI.HurewiczNormalized.normalizedSimplex line 291
  44. def OAI.HurewiczNormalized.differenceMap line 309
  45. lemma OAI.HurewiczNormalized.difference_generator line 312
  46. lemma OAI.HurewiczNormalized.difference_cycle line 319
  47. def OAI.HurewiczNormalized.toCycles line 328
  48. def OAI.HurewiczNormalized.toHomology line 332
  49. lemma OAI.HurewiczNormalized.difference_homology line 335
  50. lemma OAI.HurewiczNormalized.cycles_toHomology line 341
  51. instance OAI.HurewiczNormalized.toHomology_epi line 349
  52. lemma OAI.HurewiczNormalized.generator_toHomology line 352
  53. theorem OAI.HurewiczNormalized.canonical_span line 360