OAI/Combinatorics/CompleteCrossing/DiskChords.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Exterior polygonal replacement, ordered passages, and injective middle paths.

  1. theorem OAI.Paper170Geometry.drawing_exterior_polygonal_replacement line 18
  2. structure OAI.Paper170Geometry.PolygonalExterior line 49
  3. theorem OAI.Paper170Geometry.nonempty_polygonalExterior line 56
  4. theorem OAI.Paper170Geometry.PolygonalExterior.outside_open_disks line 72
  5. theorem OAI.Paper170Geometry.PolygonalExterior.avoids_new_vertices line 85
  6. theorem OAI.Paper170Geometry.PolygonalExterior.parameter_endpoint_of_mem_disk line 93
  7. theorem OAI.Paper170Geometry.PolygonalExterior.chord_parameter_endpoint line 120
  8. theorem OAI.Paper170Geometry.PolygonalExterior.exterior_chord_meeting_parameters line 133
  9. theorem OAI.Paper170Geometry.PolygonalExterior.exterior_spoke_meeting_parameters line 171
  10. def OAI.Paper170Geometry.DrawingPassages.orderedArc line 211
  11. theorem OAI.Paper170Geometry.DrawingPassages.orderedArc_val line 214
  12. theorem OAI.Paper170Geometry.DrawingPassages.orderedArc_inj line 219
  13. theorem OAI.Paper170Geometry.DrawingPassages.orderedArc_first line 225
  14. theorem OAI.Paper170Geometry.DrawingPassages.orderedArc_last line 229
  15. def OAI.Paper170Geometry.DrawingPassages.orderedInner line 233
  16. theorem OAI.Paper170Geometry.DrawingPassages.orderedInner_incoming line 237
  17. theorem OAI.Paper170Geometry.DrawingPassages.orderedInner_outgoing line 246
  18. theorem OAI.Paper170Geometry.DrawingPassages.orderedInner_inj line 255
  19. def OAI.Paper170Geometry.PolygonalExterior.orderedPath line 265
  20. def OAI.Paper170Geometry.PolygonalExterior.orderedBridge line 269
  21. theorem OAI.Paper170Geometry.PolygonalExterior.orderedBridge_apply line 272
  22. theorem OAI.Paper170Geometry.PolygonalExterior.orderedBridge_range line 284
  23. def OAI.Paper170Geometry.PolygonalExterior.middlePath line 290
  24. theorem OAI.Paper170Geometry.PolygonalExterior.middlePath_injective line 311
  25. theorem OAI.Paper170Geometry.PolygonalExterior.middlePath_range_iff line 349
  26. theorem OAI.Paper170Geometry.DrawingPassages.vertex_spoke_range_in_disk line 402
  27. theorem OAI.Paper170Geometry.DrawingPassages.vertex_spokes_disjoint_of_vertices_ne line 414
  28. theorem OAI.Paper170Geometry.PolygonalExterior.middle_spoke_meeting line 427
  29. def OAI.Paper170Geometry.PolygonalExterior.anchoredMiddle line 440
  30. theorem OAI.Paper170Geometry.PolygonalExterior.anchoredMiddle_range line 445
  31. theorem OAI.Paper170Geometry.PolygonalExterior.anchoredMiddle_injective line 448