OAI/Combinatorics/CompleteCrossing/Ports.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Isolated drawing disks, retained arcs, and boundary ports.

  1. abbrev OAI.Paper170Geometry.DrawingMark line 19
  2. theorem OAI.Paper170Geometry.drawing_disk_isolation line 21
  3. structure OAI.Paper170Geometry.DrawingPassages line 54

    Source documentation

    Geometric cut data for the original drawing. Existence is proved below; this record asserts no crossing bound or drawing-normalization conclusion.

    structure DrawingPassages (D : FiniteIntersectionDrawing graph) where
…

    Mentions: OAI.Paper170Geometry.FiniteIntersectionDrawing

  4. theorem OAI.Paper170Geometry.nonempty_drawingPassages line 71
  5. abbrev OAI.Paper170Geometry.DrawingPassages.ArcIndex line 128
  6. theorem OAI.Paper170Geometry.DrawingPassages.node_mark line 130
  7. def OAI.Paper170Geometry.DrawingPassages.arcStartMark line 136
  8. def OAI.Paper170Geometry.DrawingPassages.arcEndMark line 139
  9. def OAI.Paper170Geometry.DrawingPassages.arcStart line 142
  10. def OAI.Paper170Geometry.DrawingPassages.arcEnd line 145
  11. def OAI.Paper170Geometry.DrawingPassages.arc line 148
  12. theorem OAI.Paper170Geometry.DrawingPassages.arc_gap line 151
  13. theorem OAI.Paper170Geometry.DrawingPassages.arc_injective line 155
  14. theorem OAI.Paper170Geometry.DrawingPassages.arc_endpoints_ne line 158
  15. theorem OAI.Paper170Geometry.DrawingPassages.arc_range line 162
  16. theorem OAI.Paper170Geometry.DrawingPassages.arc_avoids_marks line 166
  17. theorem OAI.Paper170Geometry.DrawingPassages.retained_parameter_outside line 175
  18. theorem OAI.Paper170Geometry.DrawingPassages.arc_interior_outside line 202
  19. theorem OAI.Paper170Geometry.DrawingPassages.arc_start_on_circle line 207
  20. theorem OAI.Paper170Geometry.DrawingPassages.arc_end_on_circle line 212
  21. theorem OAI.Paper170Geometry.DrawingPassages.arcs_pairwise_disjoint line 232
  22. abbrev OAI.Paper170Geometry.DrawingPassages.Port line 272
  23. def OAI.Paper170Geometry.DrawingPassages.portPoint line 274
  24. def OAI.Paper170Geometry.DrawingPassages.portMark line 277
  25. theorem OAI.Paper170Geometry.DrawingPassages.portPoint_mem_arc line 280
  26. theorem OAI.Paper170Geometry.DrawingPassages.portPoint_injective line 287
  27. theorem OAI.Paper170Geometry.DrawingPassages.portPoint_on_circle line 303
  28. abbrev OAI.Paper170Geometry.DrawingPassages.PortsAt line 310
  29. theorem OAI.Paper170Geometry.DrawingPassages.portsAt_on_circle line 312