OAI/Combinatorics/CompleteCrossing/DiskFilling.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

Interior disk passages, vertex ports, filling containment, and crossing uniqueness.

  1. abbrev OAI.Paper170Geometry.DrawingPassages.InnerIndex line 20
  2. def OAI.Paper170Geometry.DrawingPassages.innerMark line 23
  3. def OAI.Paper170Geometry.DrawingPassages.incomingArc line 26
  4. def OAI.Paper170Geometry.DrawingPassages.outgoingArc line 29
  5. def OAI.Paper170Geometry.DrawingPassages.incomingPort line 32
  6. def OAI.Paper170Geometry.DrawingPassages.outgoingPort line 33
  7. theorem OAI.Paper170Geometry.DrawingPassages.incoming_node line 35
  8. theorem OAI.Paper170Geometry.DrawingPassages.outgoing_node line 42
  9. theorem OAI.Paper170Geometry.DrawingPassages.incomingPort_mark line 45
  10. theorem OAI.Paper170Geometry.DrawingPassages.outgoingPort_mark line 51
  11. theorem OAI.Paper170Geometry.DrawingPassages.incomingPort_point line 54
  12. theorem OAI.Paper170Geometry.DrawingPassages.outgoingPort_point line 59
  13. theorem OAI.Paper170Geometry.DrawingPassages.inner_parameter_interior line 62
  14. theorem OAI.Paper170Geometry.DrawingPassages.innerMark_is_crossing line 70
  15. def OAI.Paper170Geometry.DrawingPassages.crossingChord line 78
  16. theorem OAI.Paper170Geometry.DrawingPassages.crossingChord_injective line 82
  17. def OAI.Paper170Geometry.DrawingPassages.vertexMark line 104
  18. theorem OAI.Paper170Geometry.DrawingPassages.vertexMark_injective line 107
  19. theorem OAI.Paper170Geometry.DrawingPassages.exists_drawing_vertex_placement line 111
  20. theorem OAI.Paper170Geometry.DrawingPassages.vertex_spoke_injective line 134
  21. theorem OAI.Paper170Geometry.DrawingPassages.vertex_spoke_interior line 145
  22. theorem OAI.Paper170Geometry.DrawingPassages.innerIndex_eq_of_edge_mark line 168
  23. theorem OAI.Paper170Geometry.DrawingPassages.incomingPort_injective line 178
  24. theorem OAI.Paper170Geometry.DrawingPassages.outgoingPort_injective line 184
  25. theorem OAI.Paper170Geometry.DrawingPassages.incomingPort_ne_outgoingPort line 190
  26. theorem OAI.Paper170Geometry.DrawingPassages.incomingPoint_on_circle line 196
  27. theorem OAI.Paper170Geometry.DrawingPassages.outgoingPoint_on_circle line 200
  28. theorem OAI.Paper170Geometry.DrawingPassages.crossing_chords_transverse_at_mark line 204
  29. theorem OAI.Paper170Geometry.DrawingPassages.innerMark_no_triples line 220
  30. def OAI.Paper170Geometry.DrawingPassages.firstArc line 255
  31. def OAI.Paper170Geometry.DrawingPassages.lastArc line 258
  32. theorem OAI.Paper170Geometry.DrawingPassages.lastArc_node line 261
  33. theorem OAI.Paper170Geometry.DrawingPassages.firstArc_mark line 268
  34. theorem OAI.Paper170Geometry.DrawingPassages.lastArc_mark line 274
  35. def OAI.Paper170Geometry.DrawingPassages.startPortAt line 280
  36. def OAI.Paper170Geometry.DrawingPassages.endPortAt line 283
  37. theorem OAI.Paper170Geometry.round_chord_in_disk line 300
  38. theorem OAI.Paper170Geometry.DrawingPassages.crossingChord_range_subset_disk line 318
  39. theorem OAI.Paper170Geometry.DrawingPassages.crossingChord_interior_in_disk line 325
  40. theorem OAI.Paper170Geometry.DrawingPassages.crossingChords_disjoint_of_marks_ne line 333
  41. theorem OAI.Paper170Geometry.DrawingPassages.portPoint_outside_other_disk line 338
  42. theorem OAI.Paper170Geometry.DrawingPassages.portPoint_outside_open_disks line 345
  43. theorem OAI.Paper170Geometry.DrawingPassages.crossingChord_avoids_vertex_disks line 353
  44. theorem OAI.Paper170Geometry.DrawingPassages.innerIndex_at_mark_pair line 377
  45. def OAI.Paper170Geometry.DrawingPassages.chordCrossingsAt line 386
  46. theorem OAI.Paper170Geometry.DrawingPassages.chordCrossingsAt_subsingleton line 390
  47. theorem OAI.Paper170Geometry.DrawingPassages.chord_meeting_marks_eq line 404
  48. def OAI.Paper170Geometry.DrawingPassages.chordCrossings line 410
  49. theorem OAI.Paper170Geometry.DrawingPassages.chord_crossing_original_mark line 413
  50. def OAI.Paper170Geometry.DrawingPassages.chordCrossingOrigin line 435
  51. theorem OAI.Paper170Geometry.DrawingPassages.chordCrossingOrigin_mapsTo line 438
  52. theorem OAI.Paper170Geometry.DrawingPassages.chordCrossingOrigin_injOn line 444
  53. theorem OAI.Paper170Geometry.DrawingPassages.chordCrossings_finite line 457
  54. theorem OAI.Paper170Geometry.DrawingPassages.chordCrossings_ncard_le line 462

    Source documentation

    Different original crossing disks remain separately counted, even when their two chords come from the same pair of graph edges.

    theorem chordCrossings_ncard_le (C : DrawingPassages D) :
    C.chordCrossings.ncard ≤ finiteCrossingCount D := by
…

    Mentions: OAI.Paper170Geometry.DrawingPassages, OAI.Paper170Geometry.finiteCrossingCount