OAI/Combinatorics/CompleteCrossing/DrawingMarks.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Marked subdivision parameters, incidence graphs, and edge walks.

  1. def OAI.Paper170Geometry.drawingMarks line 24
  2. theorem OAI.Paper170Geometry.drawingMarks_finite line 27
  3. theorem OAI.Paper170Geometry.crossing_not_vertex line 30
  4. theorem OAI.Paper170Geometry.marked_parameters_finite line 36
  5. theorem OAI.Paper170Geometry.marked_parameter_zero line 40
  6. theorem OAI.Paper170Geometry.marked_parameter_one line 44
  7. theorem OAI.Paper170Geometry.unmarked_edge_point_interior line 48
  8. theorem OAI.Paper170Geometry.unmarked_intersection_same_edge line 61
  9. theorem OAI.Paper170Geometry.exists_sorted_drawing_parameters line 83
  10. theorem OAI.Paper170Geometry.exists_marked_polygonal_subdivision line 106
  11. theorem OAI.Paper170Geometry.subdivision_mark_endpoint line 128
  12. theorem OAI.Paper170Geometry.drawing_curve_meeting_mark line 153
  13. abbrev OAI.Paper170Geometry.DrawingPiece line 176
  14. def OAI.Paper170Geometry.drawingPieceStart line 179
  15. def OAI.Paper170Geometry.drawingPieceEnd line 182
  16. theorem OAI.Paper170Geometry.drawingPiece_endpoints_ne line 185
  17. theorem OAI.Paper170Geometry.drawing_pieces_meeting_endpoints line 192
  18. def OAI.Paper170Geometry.drawingSubdivisionGraph line 227
  19. theorem OAI.Paper170Geometry.drawingSubdivisionGraph_piece_adj line 239
  20. theorem OAI.Paper170Geometry.common_endpoint_alternatives line 244
  21. theorem OAI.Paper170Geometry.drawingSubdivisionGraph_embedding line 252
  22. theorem OAI.Paper170Geometry.drawingSubdivisionGraph_finite_support line 283
  23. theorem OAI.Paper170Geometry.subdivision_point_endpoint line 308
  24. theorem OAI.Paper170Geometry.drawingSubdivisionGraph_point_endpoint line 318
  25. theorem OAI.Paper170Geometry.drawingEdgeSequence_adj line 344
  26. def OAI.Paper170Geometry.drawingEdgeWalk line 353
  27. theorem OAI.Paper170Geometry.drawingEdgeWalk_length line 358
  28. theorem OAI.Paper170Geometry.drawingEdgeWalk_getVert line 362
  29. theorem OAI.Paper170Geometry.drawingEdgeWalk_isPath line 368
  30. theorem OAI.Paper170Geometry.drawingEdgeWalk_uniqueVisit line 381
  31. theorem OAI.Paper170Geometry.drawingEdgeWalk_range_eq line 401
  32. theorem OAI.Paper170Geometry.graphWalkPath_range_cases line 440
  33. theorem OAI.Paper170Geometry.drawingEdgeWalk_take_trace line 452
  34. theorem OAI.Paper170Geometry.drawingEdgeWalk_drop_trace line 478