OAI/GroupTheory/UniversalGroup/GraphActions.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.UniversalFInfinity.GraphBundle.edgeImage_edge_slice line 26
  2. lemma OAI.UniversalFInfinity.GraphBundle.edge_injective line 77
  3. lemma OAI.UniversalFInfinity.GraphBundle.edge_closedMap line 101
  4. lemma OAI.UniversalFInfinity.GraphBundle.edge_closedEmbedding line 114
  5. lemma OAI.UniversalFInfinity.GraphBundle.hom_ext line 130
  6. def OAI.UniversalFInfinity.GraphBundle.homotopyPaths line 149
  7. def OAI.UniversalFInfinity.GraphBundle.homotopy line 155
  8. def OAI.UniversalFInfinity.PathFamilies.intervalPath line 182
  9. def OAI.UniversalFInfinity.PathFamilies.unpause line 188
  10. lemma OAI.UniversalFInfinity.PathFamilies.transRefl_natural line 190
  11. lemma OAI.UniversalFInfinity.PathFamilies.continuous_transRefl line 193
  12. def OAI.UniversalFInfinity.GraphBundle.edgePath line 210
  13. lemma OAI.UniversalFInfinity.GraphBundle.edgePath_continuous line 217
  14. def OAI.UniversalFInfinity.GraphBundle.pausedEdge line 220
  15. lemma OAI.UniversalFInfinity.GraphBundle.pausedEdge_continuous line 222
  16. def OAI.UniversalFInfinity.GraphBundle.pause line 227
  17. lemma OAI.UniversalFInfinity.GraphBundle.pause_vertex line 232
  18. lemma OAI.UniversalFInfinity.GraphBundle.pause_edge line 233
  19. def OAI.UniversalFInfinity.GraphBundle.pauseVertexHomotopy line 236
  20. lemma OAI.UniversalFInfinity.GraphBundle.pauseEdgeHomotopy_continuous line 241
  21. def OAI.UniversalFInfinity.GraphBundle.pauseEdgeHomotopy line 250
  22. def OAI.UniversalFInfinity.GraphBundle.pauseHomotopy line 260
  23. def OAI.UniversalFInfinity.GraphBundle.homogeneousMap line 277
  24. lemma OAI.UniversalFInfinity.GraphBundle.homogeneousMap_vertex line 285
  25. lemma OAI.UniversalFInfinity.GraphBundle.homogeneousMap_edge line 289
  26. def OAI.UniversalFInfinity.GraphBundle.actionMap line 306
  27. lemma OAI.UniversalFInfinity.GraphBundle.actionMap_vertex line 308
  28. lemma OAI.UniversalFInfinity.GraphBundle.actionMap_edge line 311
  29. def OAI.UniversalFInfinity.GraphBundle.graphAction line 317
  30. lemma OAI.UniversalFInfinity.GraphBundle.graphAction_continuous line 332