OAI/Combinatorics/CompleteCrossing/Deletion.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Vertex deletion, its crossing-count identity, and small complete graphs.

  1. structure OAI.Paper170.VertexDeletion line 15
  2. lemma OAI.Paper170.crossingCount_zero_of_subsingleton line 33
  3. lemma OAI.Paper170.ordinaryCrossingNumber_zero_of_subsingleton line 43
  4. theorem OAI.Paper170.complete_graph_small_orders line 52
  5. def OAI.Paper170.deletionEdge line 87
  6. lemma OAI.Paper170.deletionEdge_injective line 90
  7. lemma OAI.Paper170.deletionEdge_range line 98
  8. def OAI.Paper170.deleteContinuousDrawing line 111
  9. lemma OAI.Paper170.deletion_crossings_subset line 120
  10. def OAI.Paper170.deleteDrawing line 126
  11. lemma OAI.Paper170.deleteDrawing_spec line 136
  12. lemma OAI.Paper170.deletion_crossing_iff line 144
  13. lemma OAI.Paper170.crossing_endpoints_distinct line 188
  14. lemma OAI.Paper170.deletion_survivor_card line 199
  15. lemma OAI.Paper170.deleteDrawing_count_filter line 217
  16. theorem OAI.Paper170.vertex_deletion_count line 227