OAI/Combinatorics/CompleteCrossing/RadialTracks.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Radial track displacements and connector clearance from other disks and tracks.

  1. theorem OAI.Paper170Geometry.dot2_scaled_self line 18
  2. theorem OAI.Paper170Geometry.VertexTruncation.start_radial_dot_pos line 25
  3. theorem OAI.Paper170Geometry.VertexTruncation.end_radial_dot_neg line 43
  4. theorem OAI.Paper170Geometry.VertexTruncation.bend_ne_zero line 66
  5. theorem OAI.Paper170Geometry.VertexTruncation.exists_forward_radius line 71
  6. theorem OAI.Paper170Geometry.VertexTruncation.shifted_first_piece_exterior line 93
  7. theorem OAI.Paper170Geometry.VertexTruncation.shifted_last_piece_exterior line 112
  8. theorem OAI.Paper170Geometry.det2_segmentPoint_sub line 153
  9. theorem OAI.Paper170Geometry.segment_line_level_zero line 158
  10. theorem OAI.Paper170Geometry.VertexTruncation.spokePort_is_piece_endpoint line 165
  11. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.continuous_tangentPort line 181
  12. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.tangentPort_zero line 186
  13. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.tangentPort_level line 189
  14. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.connector_level line 194
  15. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.connector_avoids_incident_piece line 200
  16. theorem OAI.Paper170Geometry.VertexTruncation.exists_nonincident_shift_radius line 228
  17. theorem OAI.Paper170Geometry.VertexTruncation.exists_all_vertex_disk_radius line 253
  18. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.exists_connector_other_disks_radius line 293
  19. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.exists_nonincident_connector_radius line 340
  20. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.exists_all_connector_track_radius line 375