OAI/Algebra/GroupRing/GraphConeCW.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.TorsionFreeZeroDivisors.GraphConeCW.oneNonempty line 15
  2. lemma OAI.TorsionFreeZeroDivisors.GraphConeCW.zero_dimension line 16
  3. instance OAI.TorsionFreeZeroDivisors.GraphConeCW.oneCW line 20
  4. instance OAI.TorsionFreeZeroDivisors.GraphConeCW.oneT2 line 21
  5. lemma OAI.TorsionFreeZeroDivisors.GraphConeCW.one_dimension line 22
  6. instance OAI.TorsionFreeZeroDivisors.GraphConeCW.coneCW line 24
  7. instance OAI.TorsionFreeZeroDivisors.GraphConeCW.coneT2 line 25
  8. lemma OAI.TorsionFreeZeroDivisors.GraphConeCW.no_higher line 26
  9. lemma OAI.TorsionFreeZeroDivisors.GraphConeCW.finite line 30
  10. lemma OAI.TorsionFreeZeroDivisors.GraphConeCW.two_cell line 40
  11. def OAI.TorsionFreeZeroDivisors.GraphConeCW.mapOne line 45
  12. lemma OAI.TorsionFreeZeroDivisors.GraphConeCW.mapOne_vertex line 46
  13. lemma OAI.TorsionFreeZeroDivisors.GraphConeCW.mapOne_edge line 47
  14. def OAI.TorsionFreeZeroDivisors.GraphConeCW.mapCone line 50
  15. lemma OAI.TorsionFreeZeroDivisors.GraphConeCW.mapCone_one line 51
  16. lemma OAI.TorsionFreeZeroDivisors.GraphConeCW.mapCone_square line 52
  17. abbrev OAI.TorsionFreeZeroDivisors.CellPresentation.Cover line 61
  18. def OAI.TorsionFreeZeroDivisors.CellPresentation.inclusion line 62
  19. lemma OAI.TorsionFreeZeroDivisors.CellPresentation.inclusion_smul line 63
  20. def OAI.TorsionFreeZeroDivisors.CellPresentation.wordLift line 64
  21. lemma OAI.TorsionFreeZeroDivisors.CellPresentation.wordLift_ker line 70
  22. def OAI.TorsionFreeZeroDivisors.CellPresentation.sectionMap line 75
  23. lemma OAI.TorsionFreeZeroDivisors.CellPresentation.sectionMap_lift line 77
  24. lemma OAI.TorsionFreeZeroDivisors.CellPresentation.sectionMap_fst line 80
  25. lemma OAI.TorsionFreeZeroDivisors.CellPresentation.sectionMap_generator line 84
  26. def OAI.TorsionFreeZeroDivisors.CellPresentation.graphNullhomotopy line 96
  27. instance OAI.TorsionFreeZeroDivisors.CellPresentation.coverT2 line 101
  28. instance OAI.TorsionFreeZeroDivisors.CellPresentation.coverCW line 103
  29. lemma OAI.TorsionFreeZeroDivisors.CellPresentation.cover_pathConnected line 106
  30. lemma OAI.TorsionFreeZeroDivisors.CellPresentation.cover_circleFill line 114
  31. lemma OAI.TorsionFreeZeroDivisors.CellPresentation.cover_simplyConnected line 123
  32. def OAI.TorsionFreeZeroDivisors.CellPresentation.diskAttaching line 132
  33. abbrev OAI.TorsionFreeZeroDivisors.CellPresentation.Base line 134
  34. def OAI.TorsionFreeZeroDivisors.CellPresentation.projection line 135
  35. lemma OAI.TorsionFreeZeroDivisors.CellPresentation.projection_quotient line 138
  36. instance OAI.TorsionFreeZeroDivisors.CellPresentation.baseT2 line 140
  37. instance OAI.TorsionFreeZeroDivisors.CellPresentation.baseCW line 141
  38. lemma OAI.TorsionFreeZeroDivisors.CellPresentation.base_dimension line 143
  39. lemma OAI.TorsionFreeZeroDivisors.CellPresentation.base_no_higher line 145
  40. lemma OAI.TorsionFreeZeroDivisors.CellPresentation.base_finite line 147
  41. lemma OAI.TorsionFreeZeroDivisors.CellPresentation.base_two_cell line 150
  42. instance OAI.TorsionFreeZeroDivisors.CellPresentation.basePathConnected line 152
  43. def OAI.TorsionFreeZeroDivisors.CellPresentation.coverPoint line 155
  44. def OAI.TorsionFreeZeroDivisors.CellPresentation.basePoint line 156
  45. def OAI.TorsionFreeZeroDivisors.CellPresentation.fundamentalEquiv line 157
  46. lemma OAI.TorsionFreeZeroDivisors.CellPresentation.cover_no_higher line 161
  47. lemma OAI.TorsionFreeZeroDivisors.CellPresentation.contractible_cover line 167
  48. def OAI.TorsionFreeZeroDivisors.ConeCells.wordClass line 179
  49. def OAI.TorsionFreeZeroDivisors.ConeCells.wordPath line 181
  50. lemma OAI.TorsionFreeZeroDivisors.ConeCells.wordPath_equal line 183
  51. def OAI.TorsionFreeZeroDivisors.ConeCells.outerPath line 187
  52. lemma OAI.TorsionFreeZeroDivisors.ConeCells.outerPath_equal line 190
  53. def OAI.TorsionFreeZeroDivisors.ConeCells.vertexMap line 196
  54. def OAI.TorsionFreeZeroDivisors.ConeCells.edgeMap line 198
  55. lemma OAI.TorsionFreeZeroDivisors.ConeCells.edgeMap_boundary line 201
  56. def OAI.TorsionFreeZeroDivisors.ConeCells.oneMap line 210
  57. def OAI.TorsionFreeZeroDivisors.ConeCells.attaching line 212
  58. abbrev OAI.TorsionFreeZeroDivisors.ConeCells.Cover line 214
  59. def OAI.TorsionFreeZeroDivisors.ConeCells.coneMap line 215
  60. lemma OAI.TorsionFreeZeroDivisors.ConeCells.coneMap_one line 222
  61. lemma OAI.TorsionFreeZeroDivisors.ConeCells.coneMap_square line 225
  62. lemma OAI.TorsionFreeZeroDivisors.ConeCells.path_equal_of_pointwise line 227
  63. def OAI.TorsionFreeZeroDivisors.ConeCells.coneRadial line 231
  64. lemma OAI.TorsionFreeZeroDivisors.ConeCells.coneRadial_apply line 237
  65. def OAI.TorsionFreeZeroDivisors.ConeCells.coneOuter line 239
  66. lemma OAI.TorsionFreeZeroDivisors.ConeCells.map_radial line 247
  67. lemma OAI.TorsionFreeZeroDivisors.ConeCells.map_outer line 258
  68. lemma OAI.TorsionFreeZeroDivisors.ConeCells.route_equal line 268
  69. lemma OAI.TorsionFreeZeroDivisors.ConeCells.wordLift_edge line 273
  70. lemma OAI.TorsionFreeZeroDivisors.ConeCells.wordLift_triangle line 304