OAI/Combinatorics/CompleteCrossing/DartPaths.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

Drawn-edge chains, dart-path realizations, and endpoint-flag pairing.

  1. instance OAI.Paper170Geometry.(instance at line 17) line 17
  2. def OAI.Paper170Geometry.dartSourceIncident line 24
  3. def OAI.Paper170Geometry.dartTargetIncident line 27
  4. theorem OAI.Paper170Geometry.OrientedDart.symm_edge line 30
  5. def OAI.Paper170Geometry.VertexTruncation.trackChain line 48
  6. def OAI.Paper170Geometry.VertexTruncation.chordChain line 56
  7. def OAI.Paper170Geometry.TruncatedSpokeCoordinates.shiftedTrackChain line 65
  8. def OAI.Paper170Geometry.TruncatedSpokeCoordinates.connectorChain line 75
  9. def OAI.Paper170Geometry.TruncatedSpokeCoordinates.shiftedEdgeChain line 79
  10. def OAI.Paper170Geometry.TruncatedSpokeCoordinates.shiftedChordChain line 85
  11. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.shiftedEdgeChain_pieces line 89
  12. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.shiftedEdgeChain_intersection_right line 95
  13. def OAI.Paper170Geometry.VertexTruncation.dartTrackChain line 122
  14. theorem OAI.Paper170Geometry.VertexTruncation.dartTrackChain_forward_vertices line 136
  15. theorem OAI.Paper170Geometry.VertexTruncation.dartTrackChain_backward_vertices line 139
  16. theorem OAI.Paper170Geometry.VertexTruncation.dartTrackChain_pieces line 143
  17. def OAI.Paper170Geometry.TruncatedSpokeCoordinates.shiftedDartChain line 152
  18. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.shiftedDartChain_forward_vertices line 160
  19. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.shiftedDartChain_backward_vertices line 163
  20. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.shiftedDartChain_pieces line 167
  21. def OAI.Paper170Geometry.incidentCast line 186
  22. theorem OAI.Paper170Geometry.incidentCast_val line 189
  23. def OAI.Paper170Geometry.dartPassageNext line 192
  24. theorem OAI.Paper170Geometry.dartPassage_ne line 196
  25. theorem OAI.Paper170Geometry.VertexTruncation.spokePort_cast line 206
  26. def OAI.Paper170Geometry.VertexTruncation.dartCycleVertex line 209
  27. def OAI.Paper170Geometry.VertexTruncation.dartCycleBlock line 212
  28. def OAI.Paper170Geometry.VertexTruncation.dartCycleChain line 219
  29. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.shiftedPort_cast line 229
  30. def OAI.Paper170Geometry.TruncatedSpokeCoordinates.shiftedCycleVertex line 232
  31. def OAI.Paper170Geometry.TruncatedSpokeCoordinates.shiftedCycleBlock line 235
  32. def OAI.Paper170Geometry.TruncatedSpokeCoordinates.shiftedCycleChain line 242
  33. def OAI.Paper170Geometry.TruncatedSpokeCoordinates.vertexChordPairing line 265
  34. def OAI.Paper170Geometry.TruncatedSpokeCoordinates.passagePairing line 269
  35. abbrev OAI.Paper170Geometry.IncidentFlag line 289
  36. def OAI.Paper170Geometry.dartSourceFlag line 291
  37. def OAI.Paper170Geometry.dartTargetFlag line 294
  38. theorem OAI.Paper170Geometry.incidentCast_refl line 297
  39. theorem OAI.Paper170Geometry.incidentFlag_cast line 300
  40. theorem OAI.Paper170Geometry.dartPassageNext_flag line 305
  41. def OAI.Paper170Geometry.TruncatedSpokeCoordinates.flagPairing line 314
  42. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.vertexChordPairing_flags line 317
  43. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.passagePairing_flags line 328
  44. def OAI.Paper170Geometry.TruncatedSpokeCoordinates.edgeEndpointPairing line 338
  45. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.dart_endpoint_pairing line 344