OAI/Combinatorics/CompleteCrossing/Tracks.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

Truncated spoke coordinates, endpoint connections, and stable signed track intersections.

  1. def OAI.Paper170Geometry.drawingSpokeDirection line 20
  2. theorem OAI.Paper170Geometry.drawingSpokeDirection_ne_zero line 27
  3. theorem OAI.Paper170Geometry.drawingSpokeDirection_port_parallel line 39
  4. theorem OAI.Paper170Geometry.drawingSpokeScale_ne_zero line 62
  5. def OAI.Paper170Geometry.VertexTruncation.spokePort line 94
  6. def OAI.Paper170Geometry.VertexTruncation.spokeIndex line 97
  7. def OAI.Paper170Geometry.VertexTruncation.spokeDirection line 100
  8. theorem OAI.Paper170Geometry.VertexTruncation.spokeIndex_lt line 103
  9. theorem OAI.Paper170Geometry.VertexTruncation.spokeDirection_ne_zero line 109
  10. theorem OAI.Paper170Geometry.VertexTruncation.spokeDirection_eq_scale line 112
  11. theorem OAI.Paper170Geometry.VertexTruncation.spokePort_circle line 122
  12. theorem OAI.Paper170Geometry.VertexTruncation.spokePort_ne_center line 126
  13. theorem OAI.Paper170Geometry.VertexTruncation.spokeDirection_parallel line 135
  14. def OAI.Paper170Geometry.VertexTruncation.spokeScale line 142
  15. theorem OAI.Paper170Geometry.VertexTruncation.spokeScale_ne_zero line 145
  16. theorem OAI.Paper170Geometry.VertexTruncation.spokePort_injective line 150
  17. theorem OAI.Paper170Geometry.VertexTruncation.exists_distinct_edge_shift_radius line 170
  18. structure OAI.Paper170Geometry.TruncatedSpokeCoordinates line 213
  19. theorem OAI.Paper170Geometry.nonempty_truncatedSpokeCoordinates line 221
  20. def OAI.Paper170Geometry.TruncatedSpokeCoordinates.shiftedPort line 233
  21. def OAI.Paper170Geometry.TruncatedSpokeCoordinates.tangentPort line 237
  22. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.tangentPort_eq line 240
  23. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.shiftedPort_level line 249
  24. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.shiftedPort_circle line 257
  25. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.connector_strictly_outside line 264
  26. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.exists_vertex_average_radius line 273
  27. theorem OAI.Paper170Geometry.VertexTruncation.exists_all_edge_shift_radius line 303
  28. theorem OAI.Paper170Geometry.VertexTruncation.exists_uniform_track_intersections line 335
  29. def OAI.Paper170Geometry.VertexTruncation.leftIncident line 377
  30. def OAI.Paper170Geometry.VertexTruncation.rightIncident line 378
  31. theorem OAI.Paper170Geometry.VertexTruncation.vertices_first line 380
  32. theorem OAI.Paper170Geometry.VertexTruncation.vertices_last line 383
  33. theorem OAI.Paper170Geometry.VertexTruncation.spokePort_left line 386
  34. theorem OAI.Paper170Geometry.VertexTruncation.spokePort_right line 390
  35. theorem OAI.Paper170Geometry.VertexTruncation.shiftedTrack_first line 394
  36. theorem OAI.Paper170Geometry.VertexTruncation.shiftedTrack_last line 400
  37. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.continuous_shiftedPort line 423
  38. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.shiftedPort_zero line 430
  39. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.shiftedPort_ne_original line 434
  40. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.exists_endpoint_separation_radius line 443
  41. theorem OAI.Paper170Geometry.VertexTruncation.piece_subset_range line 483
  42. def OAI.Paper170Geometry.VertexTruncation.signedIntersection line 488
  43. theorem OAI.Paper170Geometry.VertexTruncation.signedIntersection_self line 491
  44. theorem OAI.Paper170Geometry.VertexTruncation.signedIntersection_swap line 494
  45. theorem OAI.Paper170Geometry.VertexTruncation.signedIntersection_zero_of_pairCrossings_empty line 501
  46. theorem OAI.Paper170Geometry.VertexTruncation.pairCrossings_pos_of_signedIntersection_ne_zero line 536
  47. theorem OAI.Paper170Geometry.VertexTruncation.signedIntersection_adjacent_zero line 543
  48. theorem OAI.Paper170Geometry.VertexTruncation.spokePort_interior line 570
  49. theorem OAI.Paper170Geometry.VertexTruncation.spokePort_piece_unique line 574