OAI/Combinatorics/TriangleRemoval/Embeddings/BirthGraph.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SharpTerminalLeave.BirthGraph line 16
  2. def OAI.SharpTerminalLeave.BirthGraph.graph line 24
  3. theorem OAI.SharpTerminalLeave.BirthGraph.graph_adj line 30
  4. theorem OAI.SharpTerminalLeave.BirthGraph.graph_adj_of_lt line 33
  5. def OAI.SharpTerminalLeave.BirthGraph.parentVertices line 42
  6. theorem OAI.SharpTerminalLeave.BirthGraph.self_not_mem_older line 44
  7. theorem OAI.SharpTerminalLeave.BirthGraph.older_eq_pair line 48
  8. theorem OAI.SharpTerminalLeave.BirthGraph.sorted_triangle line 55
  9. def OAI.SharpTerminalLeave.BirthGraph.parentType line 68
  10. def OAI.SharpTerminalLeave.BirthGraph.IsTriangle line 70
  11. def OAI.SharpTerminalLeave.BirthGraph.ExposedAt line 73
  12. def OAI.SharpTerminalLeave.BirthGraph.ExtraEdge line 78
  13. theorem OAI.SharpTerminalLeave.BirthGraph.no_repeated_exposure line 81
  14. structure OAI.SharpTerminalLeave.BirthGraph.SpawnRules line 113
  15. theorem OAI.SharpTerminalLeave.BirthGraph.older_sorted_pair line 122
  16. theorem OAI.SharpTerminalLeave.BirthGraph.first_label_repeat_extra line 129
  17. theorem OAI.SharpTerminalLeave.BirthGraph.first_label_repeat_injective_extra line 177
  18. theorem OAI.SharpTerminalLeave.BirthGraph.exists_first_repeat line 186
  19. theorem OAI.SharpTerminalLeave.BirthGraph.exposed_collision_witness line 208