OAI/Combinatorics/CompleteCrossing/SurgeryIntersections.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Surgery intersection containment, strict crossing reduction, and admissibility.

  1. theorem OAI.Paper170Geometry.segment_disjoint_of_open_containment line 16
  2. theorem OAI.Paper170Geometry.PolygonalExterior.assembled_port_not_mem_other_edge line 29
  3. theorem OAI.Paper170Geometry.PolygonalExterior.reconnection_other_edge_disjoint line 35
  4. theorem OAI.Paper170Geometry.PolygonalExterior.forward_chord_disjoint_opposite_prefix line 73
  5. theorem OAI.Paper170Geometry.PolygonalExterior.forward_chord_disjoint_opposite_suffix line 84
  6. theorem OAI.Paper170Geometry.PolygonalExterior.backward_chord_disjoint_opposite_prefix line 95
  7. theorem OAI.Paper170Geometry.PolygonalExterior.backward_chord_disjoint_opposite_suffix line 106
  8. theorem OAI.Paper170Geometry.PolygonalExterior.reconnected_paths_meeting_cases line 138
  9. theorem OAI.Paper170Geometry.PolygonalExterior.reconnected_paths_meeting_old_edges line 168
  10. theorem OAI.Paper170Geometry.PolygonalExterior.reconnectedForwardPath_meeting_other line 201
  11. theorem OAI.Paper170Geometry.PolygonalExterior.reconnectedBackwardPath_meeting_other line 213
  12. theorem OAI.Paper170Geometry.PolygonalExterior.adjacentSurgeryRoutes_meeting_other line 225
  13. theorem OAI.Paper170Geometry.PolygonalExterior.adjacentSurgeryRoutes_meeting_each_other line 245
  14. theorem OAI.Paper170Geometry.PolygonalExterior.adjacentSurgeryDrawing_crossings_subset line 281
  15. theorem OAI.Paper170Geometry.PolygonalExterior.crossingChord_meeting_is_assembled_crossing line 343
  16. theorem OAI.Paper170Geometry.PolygonalExterior.adjacentSurgeryDrawing_strict_crossing_ncard line 357
  17. theorem OAI.Paper170Geometry.PolygonalExterior.adjacentSurgeryDrawing_no_triples line 401
  18. def OAI.Paper170Geometry.PolygonalExterior.adjacentSurgeryFiniteDrawing line 503
  19. theorem OAI.Paper170Geometry.PolygonalExterior.adjacentSurgeryFiniteDrawing_count_lt line 514
  20. theorem OAI.Paper170Geometry.PolygonalExterior.exists_admissible_adjacent_surgery line 540