OAI/Combinatorics/CompleteCrossing/CrossingCuts.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Ordered crossing ports, surgery cut walks, path witnesses, and cut separation.

  1. def OAI.Paper170Geometry.crossingSurgeryGraph line 21
  2. theorem OAI.Paper170Geometry.crossingSurgeryGraph_embedding line 26
  3. theorem OAI.Paper170Geometry.exterior_le_crossingSurgeryGraph line 60
  4. theorem OAI.Paper170Geometry.crossingSurgeryGraph_reconnection_adj line 65
  5. theorem OAI.Paper170Geometry.PolygonalExterior.middlePath_contains_chord line 85
  6. theorem OAI.Paper170Geometry.PolygonalExterior.assembledEdge_contains_chord line 102
  7. theorem OAI.Paper170Geometry.PolygonalExterior.assembled_crossing_ports_ordered line 108
  8. theorem OAI.Paper170Geometry.PolygonalExterior.crossing_port_walk_indices line 115
  9. theorem OAI.Paper170Geometry.PolygonalExterior.assembled_in_crossingDisk_chord line 159
  10. theorem OAI.Paper170Geometry.PolygonalExterior.assembled_crossingDisk_owner line 177
  11. theorem OAI.Paper170Geometry.PolygonalExterior.assembled_other_edge_avoids_crossingDisk line 187
  12. theorem OAI.Paper170Geometry.DrawingPassages.crossingChord_parameter_interior line 213
  13. theorem OAI.Paper170Geometry.PolygonalExterior.assembled_crossing_disk_parameter_between line 235
  14. theorem OAI.Paper170Geometry.PolygonalExterior.assembled_crossing_port_clearance line 253
  15. theorem OAI.Paper170Geometry.PolygonalExterior.crossing_cut_traces_disjoint line 281
  16. theorem OAI.Paper170Geometry.PolygonalExterior.exists_exterior_crossing_cuts line 308
  17. def OAI.Paper170Geometry.surgeryPrefixWalk line 339
  18. def OAI.Paper170Geometry.surgerySuffixWalk line 347
  19. theorem OAI.Paper170Geometry.surgeryPrefixWalk_trace line 355
  20. theorem OAI.Paper170Geometry.surgerySuffixWalk_trace line 363
  21. structure OAI.Paper170Geometry.ExteriorCrossingCut line 386
  22. theorem OAI.Paper170Geometry.PolygonalExterior.nonempty_exteriorCrossingCut line 396
  23. def OAI.Paper170Geometry.ExteriorCrossingCut.prefixInSurgery line 411
  24. def OAI.Paper170Geometry.ExteriorCrossingCut.suffixInSurgery line 417
  25. theorem OAI.Paper170Geometry.ExteriorCrossingCut.prefixInSurgery_trace line 423
  26. theorem OAI.Paper170Geometry.ExteriorCrossingCut.suffixInSurgery_trace line 429
  27. def OAI.Paper170Geometry.walkThroughChord line 450
  28. theorem OAI.Paper170Geometry.walkThroughChord_range line 454
  29. theorem OAI.Paper170Geometry.exists_simple_path_through_chord line 460
  30. theorem OAI.Paper170Geometry.surgery_mixed_endpoints_ne line 474
  31. theorem OAI.Paper170Geometry.ExteriorCrossingCut.first_parameter_lt_one line 502
  32. theorem OAI.Paper170Geometry.ExteriorCrossingCut.last_parameter_pos line 506
  33. theorem OAI.Paper170Geometry.ExteriorCrossingCut.prefix_vertex_eq line 510
  34. theorem OAI.Paper170Geometry.ExteriorCrossingCut.suffix_vertex_eq line 518
  35. theorem OAI.Paper170Geometry.ExteriorCrossingCut.first_parameter_point line 544
  36. theorem OAI.Paper170Geometry.ExteriorCrossingCut.last_parameter_point line 549
  37. theorem OAI.Paper170Geometry.ExteriorCrossingCut.prefix_subset_edge line 554
  38. theorem OAI.Paper170Geometry.ExteriorCrossingCut.suffix_subset_edge line 560
  39. theorem OAI.Paper170Geometry.ExteriorCrossingCut.incoming_not_suffix line 566
  40. theorem OAI.Paper170Geometry.ExteriorCrossingCut.outgoing_not_prefix line 573
  41. theorem OAI.Paper170Geometry.ExteriorCrossingCut.prefix_suffix_disjoint line 580