OAI/Combinatorics/CycleDecomposition/PathDeletion.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ErdosGallai.PositiveSimplePath line 17
  2. lemma OAI.ErdosGallai.PositiveSimplePath.endpoints_ne line 24
  3. theorem OAI.ErdosGallai.endpoint_path_count line 32
  4. def OAI.ErdosGallai.EndpointPathPartition line 59
  5. def OAI.ErdosGallai.MissingEndpointTheorem line 66
  6. def OAI.ErdosGallai.PathOrCycleEdgeSet line 69
  7. def OAI.ErdosGallai.LovaszPathCyclePartition line 74
  8. def OAI.ErdosGallai.MissingLovaszTheorem line 80
  9. def OAI.ErdosGallai.evenAugmentation line 91
  10. theorem OAI.ErdosGallai.evenAugmentation_some_adj line 111
  11. theorem OAI.ErdosGallai.evenAugmentation_none_adj line 115
  12. theorem OAI.ErdosGallai.evenAugmentation_some_none line 119
  13. theorem OAI.ErdosGallai.evenAugmentation_degree line 123
  14. theorem OAI.ErdosGallai.evenAugmentation_old_odd line 137
  15. theorem OAI.ErdosGallai.trail_partition_degree_sum line 154
  16. theorem OAI.ErdosGallai.trail_partition_even_degree_iff line 183
  17. theorem OAI.ErdosGallai.odd_load_one line 201
  18. theorem OAI.ErdosGallai.tight_odd_trail_partition line 219
  19. theorem OAI.ErdosGallai.path_tail_delete_start line 279
  20. theorem OAI.ErdosGallai.path_dropLast_delete_end line 300
  21. theorem OAI.ErdosGallai.positive_avoids_of_no_incidence line 309
  22. theorem OAI.ErdosGallai.delete_vertex_from_path line 317
  23. theorem OAI.ErdosGallai.delete_vertex_boundary_edges line 378
  24. theorem OAI.ErdosGallai.delete_vertex_new_ends_ne line 409
  25. theorem OAI.ErdosGallai.delete_vertex_new_endpoint_load line 438
  26. structure OAI.ErdosGallai.SimplePathPiece line 485
  27. def OAI.ErdosGallai.SimplePathPiece.Avoiding line 495
  28. def OAI.ErdosGallai.SimplePathPiece.Meeting line 496
  29. def OAI.ErdosGallai.SimplePathPiece.DeleteIndex line 497
  30. instance OAI.ErdosGallai.SimplePathPiece.(instance at line 500) line 500
  31. instance OAI.ErdosGallai.SimplePathPiece.(instance at line 503) line 503
  32. instance OAI.ErdosGallai.SimplePathPiece.(instance at line 506) line 506
  33. def OAI.ErdosGallai.SimplePathPiece.deleted line 509
  34. def OAI.ErdosGallai.SimplePathPiece.parent line 516
  35. def OAI.ErdosGallai.SimplePathPiece.oldEnd line 520
  36. def OAI.ErdosGallai.SimplePathPiece.newEnd line 525
  37. lemma OAI.ErdosGallai.SimplePathPiece.deleted_ends line 530
  38. lemma OAI.ErdosGallai.SimplePathPiece.deleted_edges_subset line 537
  39. lemma OAI.ErdosGallai.SimplePathPiece.deleted_positive_avoids line 550
  40. lemma OAI.ErdosGallai.SimplePathPiece.deleted_disjoint line 559
  41. lemma OAI.ErdosGallai.SimplePathPiece.deleted_old_load line 577
  42. lemma OAI.ErdosGallai.SimplePathPiece.deleted_new_load line 615
  43. theorem OAI.ErdosGallai.SimplePathPiece.deleted_endpoint_load line 641
  44. theorem OAI.ErdosGallai.SimplePathPiece.deleted_union line 665
  45. theorem OAI.ErdosGallai.SimplePathPiece.deleted_positive_union line 694
  46. def OAI.ErdosGallai.SimplePathPiece.deletedInduced line 715