OAI/Combinatorics/CompleteCrossing/TwoPage.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Counting actual crossing points of the explicit two-page drawing.

  1. lemma OAI.Paper170.twoPage_meeting_chords line 16
  2. lemma OAI.Paper170.chord_meeting_alternates line 49
  3. lemma OAI.Paper170.twoPage_meeting_alternates line 61
  4. lemma OAI.Paper170.pagePoint_mem_edge line 77
  5. lemma OAI.Paper170.ordered_chord_meeting line 87
  6. def OAI.Paper170.tupleFirstEdge line 108
  7. def OAI.Paper170.tupleSecondEdge line 111
  8. lemma OAI.Paper170.tuple_edges_ne line 114
  9. lemma OAI.Paper170.tuple_point_membership line 120
  10. lemma OAI.Paper170.ordered_pair_tuple line 138
  11. lemma OAI.Paper170.crossingTuplePoint_surjOn line 156
  12. lemma OAI.Paper170.crossingTuplePoint_injOn line 169
  13. theorem OAI.Paper170.two_page_crossing_bijection line 201
  14. theorem OAI.Paper170.two_page_crossing_count line 220
  15. theorem OAI.Paper170.complete_graph_upper_drawing line 236