OAI/Combinatorics/CompleteCrossing/CycleIntersections.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Signed dart and cycle intersections, passage pairing, and endpoint averaging.

  1. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.exists_complete_edge_intersection_radius line 22
  2. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.exists_chord_edge_radius line 77
  3. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.chordChain_intersection line 145
  4. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.exists_vertex_chord_chain_radius line 151
  5. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.dart_pair_intersection line 191
  6. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.chord_dart_intersection line 226
  7. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.dart_chord_intersection line 242
  8. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.exists_dart_intersection_radius line 258
  9. theorem OAI.Paper170Geometry.PolygonalChain.intersection_join_join line 301
  10. theorem OAI.Paper170Geometry.PolygonalChain.transverse_join_join line 313
  11. def OAI.Paper170Geometry.TruncatedSpokeCoordinates.passageIntersection line 325
  12. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.exists_cycle_block_radius line 331
  13. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.exists_closed_cycle_intersection_radius line 384
  14. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.exists_vertex_pairing_radius line 445
  15. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.exists_passage_pairing_radius line 466
  16. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.closed_cycle_averaged_sum line 496
  17. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.passage_sum_eq_endpoint_sum line 552
  18. def OAI.Paper170Geometry.TruncatedSpokeCoordinates.cycleIntersectionMatrix line 571
  19. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.closed_cycle_matrix_sum line 574