OAI/Combinatorics/CompleteCrossing/Reconnection.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Crossing reconnection chords and avoidance of vertices and retained arcs.

  1. def OAI.Paper170Geometry.DrawingPassages.reconnectionStart line 18
  2. def OAI.Paper170Geometry.DrawingPassages.reconnectionEnd line 21
  3. theorem OAI.Paper170Geometry.DrawingPassages.reconnection_endpoints_ne line 24
  4. theorem OAI.Paper170Geometry.DrawingPassages.crossingChord_meeting_segmentsCrossProperly line 30
  5. theorem OAI.Paper170Geometry.DrawingPassages.reconnection_chords_disjoint line 44
  6. theorem OAI.Paper170Geometry.DrawingPassages.reconnection_endpoints_on_circle line 58
  7. theorem OAI.Paper170Geometry.DrawingPassages.reconnection_open_in_disk line 70
  8. theorem OAI.Paper170Geometry.DrawingPassages.reconnection_segment_in_disk line 92
  9. theorem OAI.Paper170Geometry.DrawingPassages.reconnection_segment_avoids_vertices line 105
  10. theorem OAI.Paper170Geometry.segment_avoids_of_affine_positive line 130
  11. theorem OAI.Paper170Geometry.crossing_reconnections_avoid_point line 142
  12. theorem OAI.Paper170Geometry.DrawingPassages.reconnection_avoids_chord_meeting line 187