OAI/Combinatorics/CompleteCrossing/CircleArcs.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

Circle segments, inversion, continuous paths, and admissibility of two-page arcs.

  1. def OAI.Paper170.chordInterior line 27
  2. structure OAI.Paper170.CircleConfiguration line 31

    Source documentation

    The source's generic circle placement, stated only in geometric terms.

    structure CircleConfiguration (n : ℕ) where
…
  3. def OAI.Paper170.twoPageRoute line 41
  4. structure OAI.Paper170.TwoPageDrawing line 47

    Source documentation

    Equality with the actual circle/chord/inversion construction.

    structure TwoPageDrawing {n : ℕ} (C : CircleConfiguration n)
    (D : AdmissibleDrawing (completeGraph n)) : Prop where
…

    Mentions: OAI.Paper170.CircleConfiguration

  5. def OAI.Paper170.lineIntersectionPoint line 52
  6. def OAI.Paper170.crossingTuplePoint line 55
  7. theorem OAI.Paper170.chordInterior_eq_unitIntervalImage line 71
  8. theorem OAI.Paper170.twoPageRoute_image line 82
  9. theorem OAI.Paper170.twoPage_edgeInterior line 90
  10. theorem OAI.Paper170.circle_points_noncollinear line 112
  11. theorem OAI.Paper170.open_chord_reverse line 124
  12. theorem OAI.Paper170.open_chords_common_start line 130
  13. theorem OAI.Paper170.circle_chord_endpoints_distinct line 142
  14. theorem OAI.Paper170.CircleConfiguration.orient_inside line 195
  15. theorem OAI.Paper170.CircleConfiguration.orient_outside line 201
  16. theorem OAI.Paper170.CircleConfiguration.alternating_cross line 209
  17. theorem OAI.Paper170.lineIntersectionPoint_eq_parameter line 219
  18. theorem OAI.Paper170.open_chords_intersection_singleton line 230
  19. theorem OAI.Paper170.circle_chord_intersection line 246
  20. theorem OAI.Paper170.inversion_zero line 301
  21. theorem OAI.Paper170.inversion_ne_zero line 304
  22. theorem OAI.Paper170.continuous_squaredLength line 308
  23. theorem OAI.Paper170.continuousAt_inversion line 312
  24. def OAI.Paper170.inversionChart line 317
  25. theorem OAI.Paper170.inversion_chart_image line 331
  26. theorem OAI.Paper170.ProperCrossing.inverted line 352
  27. theorem OAI.Paper170.squaredLength_inversion line 363
  28. theorem OAI.Paper170.chord_ne_zero line 371
  29. theorem OAI.Paper170.CircleConfiguration.chord_ne_zero line 388
  30. theorem OAI.Paper170.CircleConfiguration.chord_inside line 394
  31. theorem OAI.Paper170.CircleConfiguration.chord_mem_ne_zero line 404
  32. theorem OAI.Paper170.CircleConfiguration.inverted_chord_outside line 409
  33. theorem OAI.Paper170.segmentPoint_injective line 428
  34. theorem OAI.Paper170.continuous_segmentPoint line 434
  35. theorem OAI.Paper170.continuous_twoPageRoute line 438
  36. def OAI.Paper170.twoPagePath line 452
  37. theorem OAI.Paper170.twoPageRoute_injective line 461
  38. theorem OAI.Paper170.twoPageRoute_avoids_vertices line 477
  39. def OAI.Paper170.twoPageContinuous line 494
  40. theorem OAI.Paper170.twoPageContinuous_edgeInterior line 502
  41. theorem OAI.Paper170.CircleConfiguration.chord_proper line 520
  42. theorem OAI.Paper170.CircleConfiguration.chord_inter_finite line 535
  43. theorem OAI.Paper170.CircleConfiguration.chord_inverted_disjoint line 541
  44. theorem OAI.Paper170.twoPageContinuous_same_color line 548
  45. theorem OAI.Paper170.twoPageContinuous_inter_finite line 561
  46. theorem OAI.Paper170.twoPageContinuous_crossings_finite line 576
  47. theorem OAI.Paper170.twoPageContinuous_proper line 600
  48. theorem OAI.Paper170.twoPageContinuous_no_triples line 618
  49. def OAI.Paper170.twoPageAdmissible line 639
  50. theorem OAI.Paper170.two_page_drawing_exists line 646