OAI/GroupTheory/UniversalGroup/Cayley.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.UniversalFInfinity.Cayley.sphere_one_cases line 14
  2. instance OAI.UniversalFInfinity.Cayley.(instance at line 20) line 20
  3. instance OAI.UniversalFInfinity.Cayley.(instance at line 32) line 32
  4. def OAI.UniversalFInfinity.Cayley.minus line 34
  5. def OAI.UniversalFInfinity.Cayley.plus line 35
  6. def OAI.UniversalFInfinity.Cayley.attaching line 40
  7. abbrev OAI.UniversalFInfinity.Cayley.Graph line 43
  8. instance OAI.UniversalFInfinity.Cayley.(instance at line 45) line 45
  9. def OAI.UniversalFInfinity.Cayley.vertex line 47
  10. lemma OAI.UniversalFInfinity.Cayley.discrete_dimension line 50
  11. instance OAI.UniversalFInfinity.Cayley.graphCW line 55
  12. instance OAI.UniversalFInfinity.Cayley.(instance at line 58) line 58
  13. lemma OAI.UniversalFInfinity.Cayley.graph_dimension line 61
  14. lemma OAI.UniversalFInfinity.Cayley.vertex_injective line 64
  15. lemma OAI.UniversalFInfinity.Cayley.cell_minus line 66
  16. lemma OAI.UniversalFInfinity.Cayley.cell_plus line 73
  17. instance OAI.UniversalFInfinity.Cayley.disk_pathConnected line 80
  18. lemma OAI.UniversalFInfinity.Cayley.cell_joined line 83
  19. lemma OAI.UniversalFInfinity.Cayley.vertex_smul line 88
  20. lemma OAI.UniversalFInfinity.Cayley.vertices_joined line 90
  21. lemma OAI.UniversalFInfinity.Cayley.graph_pathConnected line 112
  22. lemma OAI.UniversalFInfinity.PathSquares.turn line 134
  23. def OAI.UniversalFInfinity.PathSquares.spanContract line 140
  24. lemma OAI.UniversalFInfinity.PathSquares.spanContract_source line 149
  25. lemma OAI.UniversalFInfinity.PathSquares.spanContract_target line 154
  26. def OAI.UniversalFInfinity.PathSquares.pauseReverse line 160
  27. theorem OAI.UniversalFInfinity.PathSquares.edgeSquare line 162
  28. def OAI.UniversalFInfinity.Cayley.edgeParam line 194
  29. lemma OAI.UniversalFInfinity.Cayley.continuous_edgeParam line 199
  30. def OAI.UniversalFInfinity.Cayley.edgeTime line 201
  31. lemma OAI.UniversalFInfinity.Cayley.continuous_edgeTime line 208
  32. lemma OAI.UniversalFInfinity.Cayley.edgeParam_time line 211
  33. lemma OAI.UniversalFInfinity.Cayley.edgeTime_param line 218
  34. lemma OAI.UniversalFInfinity.Cayley.edgeParam_zero line 222
  35. lemma OAI.UniversalFInfinity.Cayley.edgeParam_one line 226
  36. lemma OAI.UniversalFInfinity.Cayley.edgeTime_minus line 230
  37. lemma OAI.UniversalFInfinity.Cayley.edgeTime_plus line 232
  38. lemma OAI.UniversalFInfinity.Cayley.sphere_one_eq line 234
  39. def OAI.UniversalFInfinity.Cayley.edge line 242
  40. def OAI.UniversalFInfinity.Cayley.edgeSquare line 252
  41. lemma OAI.UniversalFInfinity.Cayley.edgeSquare_source line 254
  42. lemma OAI.UniversalFInfinity.Cayley.edgeSquare_target line 257
  43. def OAI.UniversalFInfinity.Cayley.edgePaths line 261
  44. def OAI.UniversalFInfinity.Cayley.vertexPaths line 265
  45. lemma OAI.UniversalFInfinity.Cayley.edgePaths_boundary line 266
  46. def OAI.UniversalFInfinity.Cayley.graphPaths line 279
  47. lemma OAI.UniversalFInfinity.Cayley.graphPaths_zero line 282
  48. lemma OAI.UniversalFInfinity.Cayley.graphPaths_one line 292
  49. def OAI.UniversalFInfinity.Cayley.graphNullhomotopy line 301
  50. theorem OAI.UniversalFInfinity.Cellular.cylinderFill line 313
  51. def OAI.UniversalFInfinity.LoopSphere.sides line 363
  52. def OAI.UniversalFInfinity.LoopSphere.ends line 364
  53. lemma OAI.UniversalFInfinity.LoopSphere.ends_sides line 367
  54. def OAI.UniversalFInfinity.LoopSphere.map line 375
  55. theorem OAI.UniversalFInfinity.LoopSphere.homotopic_of_fill line 377
  56. lemma OAI.UniversalFInfinity.LoopSphere.natural line 405
  57. lemma OAI.UniversalFInfinity.LoopSphere.homotopic_map_of_fill line 416