OAI/Combinatorics/CompleteCrossing/SpokePorts.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Chain pieces near vertices, incident spoke ports, and short vertex radii.

  1. theorem OAI.Paper170Geometry.drawing_chain_piece_vertex line 24
  2. theorem OAI.Paper170Geometry.drawing_chain_range_eq line 56
  3. theorem OAI.Paper170Geometry.drawing_chain_pieces_pos line 62
  4. theorem OAI.Paper170Geometry.drawing_chain_piece_open_subset_interior line 83
  5. theorem OAI.Paper170Geometry.exists_vertex_piece_clearance line 122
  6. theorem OAI.Paper170Geometry.drawing_chain_startPort_interior line 171
  7. theorem OAI.Paper170Geometry.drawing_chain_endPort_interior line 181
  8. theorem OAI.Paper170Geometry.drawing_chain_startPort_circle line 196
  9. theorem OAI.Paper170Geometry.drawing_chain_endPort_circle line 207
  10. theorem OAI.Paper170Geometry.exists_vertex_trace_disks line 231
  11. def OAI.Paper170Geometry.IncidentEdges line 277
  12. instance OAI.Paper170Geometry.incidentEdgesFintype line 280
  13. theorem OAI.Paper170Geometry.incident_edges_adjacent line 285
  14. def OAI.Paper170Geometry.drawingSpokePort line 294
  15. theorem OAI.Paper170Geometry.drawingSpokePort_interior line 300
  16. theorem OAI.Paper170Geometry.drawingSpokePort_circle line 315
  17. theorem OAI.Paper170Geometry.drawingSpokePort_injective line 328
  18. theorem OAI.Paper170Geometry.exists_vertex_spoke_bound line 361
  19. theorem OAI.Paper170Geometry.exists_short_vertex_radius line 396