OAI/Combinatorics/CompleteCrossing/AdjacentSurgery.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Reconnected paths and point-removing surgery on adjacent edges.

  1. theorem OAI.Paper170Geometry.surgery_forward_adj line 20
  2. theorem OAI.Paper170Geometry.surgery_backward_adj line 24
  3. def OAI.Paper170Geometry.reconnectedForwardWalk line 28
  4. def OAI.Paper170Geometry.reconnectedBackwardWalk line 34
  5. theorem OAI.Paper170Geometry.reconnectedForwardWalk_trace line 40
  6. theorem OAI.Paper170Geometry.reconnectedBackwardWalk_trace line 49
  7. def OAI.Paper170Geometry.reconnectedForwardPath line 75
  8. def OAI.Paper170Geometry.reconnectedBackwardPath line 80
  9. theorem OAI.Paper170Geometry.reconnectedForwardPath_injective line 85
  10. theorem OAI.Paper170Geometry.reconnectedBackwardPath_injective line 94
  11. theorem OAI.Paper170Geometry.reconnectedForwardPath_hasFiniteAffineCover line 103
  12. theorem OAI.Paper170Geometry.reconnectedBackwardPath_hasFiniteAffineCover line 109
  13. theorem OAI.Paper170Geometry.reconnectedForwardPath_trace line 115
  14. theorem OAI.Paper170Geometry.reconnectedBackwardPath_trace line 125
  15. theorem OAI.Paper170Geometry.reconnected_paths_avoid_crossing line 152
  16. theorem OAI.Paper170Geometry.path_interior_avoids_vertices_of_range line 189
  17. theorem OAI.Paper170Geometry.reconnectedForwardPath_vertex_eq line 198
  18. theorem OAI.Paper170Geometry.reconnectedBackwardPath_vertex_eq line 208
  19. theorem OAI.Paper170Geometry.reconnectedForwardPath_interior_avoids_vertices line 218
  20. theorem OAI.Paper170Geometry.reconnectedBackwardPath_interior_avoids_vertices line 230
  21. def OAI.Paper170.ContinuousDrawing.replaceTwoRoutes line 255
  22. theorem OAI.Paper170.ContinuousDrawing.replaceTwoRoutes_first line 266
  23. theorem OAI.Paper170.ContinuousDrawing.replaceTwoRoutes_second line 272
  24. theorem OAI.Paper170.ContinuousDrawing.replaceTwoRoutes_other line 278
  25. def OAI.Paper170.ContinuousDrawing.replaceTwoEdges line 285
  26. theorem OAI.Paper170.ContinuousDrawing.replaceTwoRoutes_range_cases line 335
  27. def OAI.Paper170Geometry.adjacentSurgeryRouteP line 367
  28. def OAI.Paper170Geometry.adjacentSurgeryRouteQ line 376
  29. theorem OAI.Paper170Geometry.adjacentSurgeryRouteP_injective line 385
  30. theorem OAI.Paper170Geometry.adjacentSurgeryRouteQ_injective line 394
  31. theorem OAI.Paper170Geometry.adjacentSurgeryRouteP_avoids_vertices line 403
  32. theorem OAI.Paper170Geometry.adjacentSurgeryRouteQ_avoids_vertices line 415
  33. def OAI.Paper170Geometry.adjacentSurgeryDrawing line 444
  34. theorem OAI.Paper170Geometry.adjacentSurgeryDrawing_vertex line 455
  35. theorem OAI.Paper170Geometry.adjacentSurgeryDrawing_first line 461
  36. theorem OAI.Paper170Geometry.adjacentSurgeryDrawing_second line 468
  37. theorem OAI.Paper170Geometry.adjacentSurgeryDrawing_other line 475
  38. theorem OAI.Paper170Geometry.adjacentSurgeryRouteP_hasFiniteAffineCover line 483
  39. theorem OAI.Paper170Geometry.adjacentSurgeryRouteQ_hasFiniteAffineCover line 492
  40. theorem OAI.Paper170Geometry.adjacentSurgeryDrawing_hasFiniteAffineCover line 518
  41. theorem OAI.Paper170Geometry.adjacentSurgeryRoutes_avoid_crossing line 536
  42. theorem OAI.Paper170Geometry.adjacentSurgeryDrawing_avoids_crossing line 553
  43. theorem OAI.Paper170Geometry.PolygonalExterior.exists_adjacentSurgery_continuousDrawing line 590