OAI/Combinatorics/CompleteCrossing/Truncation.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Vertex-disk truncation, retained crossings, reduced corners, and transverse segments.

  1. theorem OAI.Paper170Geometry.LocallyStraightAt.exists_trace_line line 27
  2. theorem OAI.Paper170Geometry.minimum_bend_not_locallyStraight line 45
  3. theorem OAI.Paper170Geometry.minimum_bend_not_crossing line 62
  4. theorem OAI.Paper170Geometry.minimum_vertices_not_crossing line 78
  5. theorem OAI.Paper170Geometry.minimum_piece_crossing_open line 97
  6. theorem OAI.Paper170Geometry.truncated_piece_vertex_disk_cases line 135
  7. theorem OAI.Paper170Geometry.truncated_path_vertex_disk_cases line 174
  8. theorem OAI.Paper170Geometry.LocallyTransverseCrossings.exists_trace_lines line 206
  9. theorem OAI.Paper170Geometry.minimum_piece_det_at_crossing line 231
  10. theorem OAI.Paper170Geometry.drawing_edge_trace_decomposition line 270
  11. theorem OAI.Paper170Geometry.vertex_disks_crossing_free line 322
  12. theorem OAI.Paper170Geometry.crossing_mem_truncated_edge line 361
  13. theorem OAI.Paper170Geometry.truncated_range_subset_edgeInterior line 401
  14. theorem OAI.Paper170Geometry.truncated_edge_intersections_eq line 431
  15. theorem OAI.Paper170Geometry.truncated_vertices_not_crossing line 473
  16. theorem OAI.Paper170Geometry.truncated_segment_pair_transverse line 513
  17. structure OAI.Paper170Geometry.VertexTruncation line 576
  18. theorem OAI.Paper170Geometry.nonempty_vertexTruncation line 592
  19. def OAI.Paper170Geometry.VertexTruncation.pieces line 608
  20. def OAI.Paper170Geometry.VertexTruncation.vertices line 610
  21. def OAI.Paper170Geometry.VertexTruncation.startPort line 612
  22. def OAI.Paper170Geometry.VertexTruncation.endPort line 614
  23. theorem OAI.Paper170Geometry.VertexTruncation.pieces_pos line 616
  24. theorem OAI.Paper170Geometry.VertexTruncation.weak_short line 618
  25. def OAI.Paper170Geometry.VertexTruncation.path line 623
  26. theorem OAI.Paper170Geometry.VertexTruncation.path_injective line 626
  27. theorem OAI.Paper170Geometry.VertexTruncation.path_hasFiniteAffineCover line 630
  28. theorem OAI.Paper170Geometry.VertexTruncation.range_subset_edgeInterior line 633
  29. theorem OAI.Paper170Geometry.VertexTruncation.direction_ne_zero line 636
  30. theorem OAI.Paper170Geometry.VertexTruncation.offset_avoidance line 655
  31. theorem OAI.Paper170Geometry.VertexTruncation.edge_intersections_eq line 662
  32. theorem OAI.Paper170Geometry.VertexTruncation.pair_transverse line 667
  33. theorem OAI.Paper170Geometry.VertexTruncation.crossing_free_disks line 675
  34. theorem OAI.Paper170Geometry.VertexTruncation.vertices_not_crossing line 680
  35. theorem OAI.Paper170Geometry.VertexTruncation.vertex_disk_cases line 685
  36. theorem OAI.Paper170Geometry.normalized_vertexTruncation line 695