OAI/GroupTheory/UniversalGroup/TreeGeometry.lean

GitHub source file

86 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniversalFInfinity.PathFamilies.diagonalSquare line 23
  2. lemma OAI.UniversalFInfinity.PathFamilies.diagonalSquare_zero_left line 27
  3. lemma OAI.UniversalFInfinity.PathFamilies.diagonalSquare_one_left line 33
  4. lemma OAI.UniversalFInfinity.PathFamilies.diagonalSquare_symm line 39
  5. lemma OAI.UniversalFInfinity.PathFamilies.diagonalSquare_zero_right line 43
  6. lemma OAI.UniversalFInfinity.PathFamilies.diagonalSquare_one_right line 46
  7. lemma OAI.UniversalFInfinity.PathFamilies.diagonalSquare_continuous line 50
  8. lemma OAI.UniversalFInfinity.PathFamilies.diagonalSquare_continuous_params line 58
  9. abbrev OAI.UniversalFInfinity.GraphBundle.Homogeneous line 78
  10. def OAI.UniversalFInfinity.GraphBundle.shift line 80
  11. lemma OAI.UniversalFInfinity.GraphBundle.shift_vertex line 87
  12. lemma OAI.UniversalFInfinity.GraphBundle.shift_edge line 89
  13. def OAI.UniversalFInfinity.GraphBundle.shiftVertexHomotopy line 93
  14. lemma OAI.UniversalFInfinity.GraphBundle.shiftEdge_continuous line 102
  15. def OAI.UniversalFInfinity.GraphBundle.shiftEdgeHomotopy line 118
  16. def OAI.UniversalFInfinity.GraphBundle.shiftHomotopy line 127
  17. def OAI.UniversalFInfinity.GraphBundle.shiftIterate line 132
  18. def OAI.UniversalFInfinity.GraphBundle.shiftIterateHomotopy line 135
  19. def OAI.UniversalFInfinity.GraphBundle.forward line 147
  20. lemma OAI.UniversalFInfinity.GraphBundle.forward_natural line 151
  21. lemma OAI.UniversalFInfinity.GraphBundle.shiftIterate_vertex line 159
  22. lemma OAI.UniversalFInfinity.GraphBundle.shiftIterate_edge line 168
  23. lemma OAI.UniversalFInfinity.Milnor.iterateHom_comm line 182
  24. def OAI.UniversalFInfinity.TorusGeometry.forwardOffset line 194
  25. lemma OAI.UniversalFInfinity.TorusGeometry.forward_eq line 197
  26. lemma OAI.UniversalFInfinity.TorusGeometry.forward_naturality line 215
  27. lemma OAI.UniversalFInfinity.TorusGeometry.stage_shift_vertex line 222
  28. lemma OAI.UniversalFInfinity.TorusGeometry.stage_shift_edge line 229
  29. def OAI.UniversalFInfinity.DirectedGraph.attaching line 243
  30. abbrev OAI.UniversalFInfinity.DirectedGraph.Graph line 245
  31. def OAI.UniversalFInfinity.DirectedGraph.vertex line 246
  32. lemma OAI.UniversalFInfinity.DirectedGraph.discrete_dimension line 248
  33. instance OAI.UniversalFInfinity.DirectedGraph.graphCW line 252
  34. instance OAI.UniversalFInfinity.DirectedGraph.(instance at line 253) line 253
  35. lemma OAI.UniversalFInfinity.DirectedGraph.graph_dimension line 254
  36. lemma OAI.UniversalFInfinity.DirectedGraph.cell_minus line 258
  37. lemma OAI.UniversalFInfinity.DirectedGraph.cell_plus line 261
  38. def OAI.UniversalFInfinity.DirectedGraph.edge line 264
  39. def OAI.UniversalFInfinity.DirectedGraph.edgeSquare line 274
  40. lemma OAI.UniversalFInfinity.DirectedGraph.edgeSquare_source line 277
  41. lemma OAI.UniversalFInfinity.DirectedGraph.edgeSquare_target line 280
  42. def OAI.UniversalFInfinity.DirectedGraph.edgePaths line 283
  43. def OAI.UniversalFInfinity.DirectedGraph.vertexPaths line 287
  44. lemma OAI.UniversalFInfinity.DirectedGraph.edgePaths_boundary line 288
  45. def OAI.UniversalFInfinity.DirectedGraph.graphPaths line 300
  46. lemma OAI.UniversalFInfinity.DirectedGraph.graphPaths_zero line 302
  47. lemma OAI.UniversalFInfinity.DirectedGraph.graphPaths_one line 310
  48. def OAI.UniversalFInfinity.DirectedGraph.graphNullhomotopy line 317
  49. lemma OAI.UniversalFInfinity.DirectedTree.height_iterate line 331
  50. def OAI.UniversalFInfinity.DirectedTree.rayProduct line 337
  51. lemma OAI.UniversalFInfinity.DirectedTree.rayProduct_add line 341
  52. lemma OAI.UniversalFInfinity.DirectedTree.rayProduct_first line 351
  53. lemma OAI.UniversalFInfinity.DirectedTree.route_independent line 358
  54. def OAI.UniversalFInfinity.DirectedTree.potential line 376
  55. lemma OAI.UniversalFInfinity.DirectedTree.potential_route line 382
  56. lemma OAI.UniversalFInfinity.DirectedTree.potential_edge line 388
  57. lemma OAI.UniversalFInfinity.DirectedGraph.ray_joined line 406
  58. lemma OAI.UniversalFInfinity.DirectedGraph.vertex_joined line 415
  59. def OAI.UniversalFInfinity.DirectedGraph.initialPath line 421
  60. def OAI.UniversalFInfinity.DirectedGraph.initialClass line 424
  61. def OAI.UniversalFInfinity.DirectedGraph.edgeClass line 427
  62. def OAI.UniversalFInfinity.DirectedGraph.edgeWeight line 430
  63. def OAI.UniversalFInfinity.DirectedGraph.treeClass line 434
  64. lemma OAI.UniversalFInfinity.DirectedGraph.treeClass_edge line 440
  65. def OAI.UniversalFInfinity.DirectedGraph.treePath line 450
  66. lemma OAI.UniversalFInfinity.DirectedGraph.treePath_edge line 455
  67. lemma OAI.UniversalFInfinity.DirectedGraph.tree_contractible line 466
  68. def OAI.UniversalFInfinity.GraphBundle.treeProjection line 485
  69. lemma OAI.UniversalFInfinity.GraphBundle.treeProjection_vertex line 490
  70. lemma OAI.UniversalFInfinity.GraphBundle.treeProjection_edge line 492
  71. lemma OAI.UniversalFInfinity.GraphBundle.pathMap_boundary line 497
  72. def OAI.UniversalFInfinity.GraphBundle.treePathMap line 506
  73. lemma OAI.UniversalFInfinity.GraphBundle.treePathMap_vertex line 510
  74. lemma OAI.UniversalFInfinity.GraphBundle.treePathMap_edge line 512
  75. lemma OAI.UniversalFInfinity.GraphBundle.nullhomotopic_of_fiber_constant line 519
  76. def OAI.UniversalFInfinity.GraphBundle.connectorPath line 553
  77. lemma OAI.UniversalFInfinity.GraphBundle.connectorPath_continuous line 561
  78. def OAI.UniversalFInfinity.GraphBundle.gluedPath line 567
  79. lemma OAI.UniversalFInfinity.GraphBundle.gluedPath_continuous line 572
  80. lemma OAI.UniversalFInfinity.GraphBundle.gluedPath_zero line 585
  81. def OAI.UniversalFInfinity.GraphBundle.collapsed line 596
  82. lemma OAI.UniversalFInfinity.GraphBundle.collapsed_edge line 601
  83. def OAI.UniversalFInfinity.GraphBundle.gluedEdgeHomotopy line 605
  84. def OAI.UniversalFInfinity.GraphBundle.gluedVertexHomotopy line 614
  85. def OAI.UniversalFInfinity.GraphBundle.coherentHomotopy line 618
  86. theorem OAI.UniversalFInfinity.GraphBundle.nullhomotopic_of_coherent_contraction line 626