OAI/Combinatorics/CycleDecomposition/Lovasz.lean

GitHub source file

131 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ErdosGallai.Lovasz.StarActive line 19
  2. lemma OAI.ErdosGallai.Lovasz.starActive_source line 22
  3. lemma OAI.ErdosGallai.Lovasz.starActive_step line 26
  4. lemma OAI.ErdosGallai.Lovasz.starActive_iff line 31
  5. lemma OAI.ErdosGallai.Lovasz.starActive_original_iff line 42
  6. lemma OAI.ErdosGallai.Lovasz.starActive_subset line 49
  7. lemma OAI.ErdosGallai.Lovasz.starActive_no_loop line 57
  8. lemma OAI.ErdosGallai.Lovasz.star_inj line 70
  9. structure OAI.ErdosGallai.Lovasz.PathPiece line 78
  10. lemma OAI.ErdosGallai.Lovasz.PathPiece.ends_ne line 85
  11. structure OAI.ErdosGallai.Lovasz.Piece line 92
  12. def OAI.ErdosGallai.Lovasz.Piece.ofPath line 102
  13. def OAI.ErdosGallai.Lovasz.Piece.ofCycle line 105
  14. structure OAI.ErdosGallai.Lovasz.Arm line 110
  15. def OAI.ErdosGallai.Lovasz.Arm.tip line 121
  16. def OAI.ErdosGallai.Lovasz.Arm.flip line 128
  17. lemma OAI.ErdosGallai.Lovasz.Arm.flip_edges line 136
  18. lemma OAI.ErdosGallai.Lovasz.Arm.mem_flip_support line 139
  19. lemma OAI.ErdosGallai.Lovasz.Arm.two_arms_isPath line 142
  20. def OAI.ErdosGallai.Lovasz.Arm.join line 158
  21. lemma OAI.ErdosGallai.Lovasz.Arm.join_edges line 165
  22. lemma OAI.ErdosGallai.Lovasz.Arm.near_ne line 173
  23. lemma OAI.ErdosGallai.Lovasz.Arm.far_ne line 178
  24. lemma OAI.ErdosGallai.Lovasz.Arm.far_ne_center line 181
  25. lemma OAI.ErdosGallai.Lovasz.Arm.star_not_mem line 186
  26. lemma OAI.ErdosGallai.Lovasz.Arm.flip_disjoint_left line 191
  27. lemma OAI.ErdosGallai.Lovasz.Arm.flip_disjoint_right line 198
  28. def OAI.ErdosGallai.Lovasz.Arm.orient line 203
  29. lemma OAI.ErdosGallai.Lovasz.Arm.orient_edges line 206
  30. lemma OAI.ErdosGallai.Lovasz.Arm.orient_near line 214
  31. lemma OAI.ErdosGallai.Lovasz.Arm.mem_orient_support line 218
  32. lemma OAI.ErdosGallai.Lovasz.Arm.orient_disjoint line 228
  33. inductive OAI.ErdosGallai.Lovasz.Frame line 239
  34. def OAI.ErdosGallai.Lovasz.Frame.path line 247
  35. def OAI.ErdosGallai.Lovasz.Frame.Port line 252
  36. def OAI.ErdosGallai.Lovasz.Frame.endpoint line 257
  37. def OAI.ErdosGallai.Lovasz.Frame.exit line 264
  38. def OAI.ErdosGallai.Lovasz.Frame.inserted line 270
  39. def OAI.ErdosGallai.Lovasz.Frame.removed line 273
  40. lemma OAI.ErdosGallai.Lovasz.Frame.endpoint_ne_center line 276
  41. lemma OAI.ErdosGallai.Lovasz.Frame.endpoint_injective line 287
  42. lemma OAI.ErdosGallai.Lovasz.Frame.port_iff_endpoint line 301
  43. lemma OAI.ErdosGallai.Lovasz.Frame.exit_edge line 326
  44. lemma OAI.ErdosGallai.Lovasz.Frame.removed_subset line 340
  45. lemma OAI.ErdosGallai.Lovasz.Frame.removed_away line 345
  46. lemma OAI.ErdosGallai.Lovasz.Frame.removed_tip line 350
  47. lemma OAI.ErdosGallai.Lovasz.Frame.inserted_away line 354
  48. lemma OAI.ErdosGallai.Lovasz.Frame.inserted_tip line 363
  49. lemma OAI.ErdosGallai.Lovasz.Frame.inserted_through line 368
  50. lemma OAI.ErdosGallai.Lovasz.Frame.removed_through line 377
  51. lemma OAI.ErdosGallai.Lovasz.replace_two_attachments line 388
  52. lemma OAI.ErdosGallai.Lovasz.Frame.modify_through line 402
  53. lemma OAI.ErdosGallai.Lovasz.Frame.modify_tip line 438
  54. lemma OAI.ErdosGallai.Lovasz.Frame.modify_away line 464
  55. theorem OAI.ErdosGallai.Lovasz.Frame.modify line 515
  56. theorem OAI.ErdosGallai.Lovasz.rewire_partition line 527
  57. inductive OAI.ErdosGallai.Lovasz.Centered line 580
  58. def OAI.ErdosGallai.Lovasz.Centered.piece line 587
  59. def OAI.ErdosGallai.Lovasz.Centered.Port line 591
  60. def OAI.ErdosGallai.Lovasz.Centered.endpoint line 595
  61. def OAI.ErdosGallai.Lovasz.Centered.exit line 599
  62. def OAI.ErdosGallai.Lovasz.Centered.inserted line 603
  63. def OAI.ErdosGallai.Lovasz.Centered.removed line 606
  64. lemma OAI.ErdosGallai.Lovasz.Centered.exit_edge line 609
  65. lemma OAI.ErdosGallai.Lovasz.Centered.exit_adj line 615
  66. lemma OAI.ErdosGallai.Lovasz.Centered.exit_none_all line 619
  67. lemma OAI.ErdosGallai.Lovasz.Centered.removed_subset line 629
  68. lemma OAI.ErdosGallai.Lovasz.Centered.modify line 634
  69. theorem OAI.ErdosGallai.Lovasz.restore_selected line 655
  70. theorem OAI.ErdosGallai.Lovasz.restore_star line 726
  71. def OAI.ErdosGallai.Lovasz.Arm.fromWalk line 752
  72. lemma OAI.ErdosGallai.Lovasz.Arm.fromWalk_far line 759
  73. lemma OAI.ErdosGallai.Lovasz.Arm.fromWalk_support line 765
  74. lemma OAI.ErdosGallai.Lovasz.Arm.fromWalk_tip_edges line 771
  75. lemma OAI.ErdosGallai.Lovasz.PathPiece.exists_frame line 778
  76. lemma OAI.ErdosGallai.Lovasz.Piece.isTrail line 835
  77. def OAI.ErdosGallai.Lovasz.Piece.mapLe line 840
  78. lemma OAI.ErdosGallai.Lovasz.Piece.mapLe_edges line 848
  79. lemma OAI.ErdosGallai.Lovasz.Piece.mapLe_start line 853
  80. lemma OAI.ErdosGallai.Lovasz.Piece.mapLe_finish line 855
  81. lemma OAI.ErdosGallai.Lovasz.Piece.exists_centered line 858
  82. theorem OAI.ErdosGallai.Lovasz.trail_partition_degree_sum line 874
  83. theorem OAI.ErdosGallai.Lovasz.trail_partition_even_degree_iff line 903
  84. lemma OAI.ErdosGallai.Lovasz.endpoint_of_odd line 921
  85. theorem OAI.ErdosGallai.Lovasz.restore_partition line 940
  86. def OAI.ErdosGallai.Lovasz.activeOrder line 964
  87. lemma OAI.ErdosGallai.Lovasz.activeOrder_mono line 967
  88. def OAI.ErdosGallai.Lovasz.HasPartition line 973
  89. def OAI.ErdosGallai.Lovasz.evenStarVertices line 978
  90. def OAI.ErdosGallai.Lovasz.evenStarEdges line 981
  91. def OAI.ErdosGallai.Lovasz.deleteEvenStar line 984
  92. lemma OAI.ErdosGallai.Lovasz.evenStar_subset line 987
  93. lemma OAI.ErdosGallai.Lovasz.deleteEvenStar_neighbor_even line 991
  94. lemma OAI.ErdosGallai.Lovasz.deleteEvenStar_neighbor_odd line 1011
  95. lemma OAI.ErdosGallai.Lovasz.deleteEvenStar_neighbor_degree line 1025
  96. lemma OAI.ErdosGallai.Lovasz.deleteEvenStar_edges line 1039
  97. lemma OAI.ErdosGallai.Lovasz.deleteEvenStar_fresh line 1044
  98. lemma OAI.ErdosGallai.Lovasz.deleteEvenStar_lt line 1049
  99. theorem OAI.ErdosGallai.Lovasz.even_vertex_step line 1065
  100. lemma OAI.ErdosGallai.Lovasz.single_edge_piece line 1078
  101. lemma OAI.ErdosGallai.Lovasz.partition_single_edges line 1087
  102. lemma OAI.ErdosGallai.Lovasz.matching_partition line 1106
  103. def OAI.ErdosGallai.Lovasz.subdivision line 1115
  104. lemma OAI.ErdosGallai.Lovasz.subdivision_some line 1134
  105. lemma OAI.ErdosGallai.Lovasz.subdivision_none_some line 1136
  106. lemma OAI.ErdosGallai.Lovasz.subdivision_some_none line 1138
  107. lemma OAI.ErdosGallai.Lovasz.subdivision_none_none line 1140
  108. def OAI.ErdosGallai.Lovasz.halfSubdivision line 1143
  109. lemma OAI.ErdosGallai.Lovasz.half_some line 1146
  110. lemma OAI.ErdosGallai.Lovasz.half_none_some line 1151
  111. lemma OAI.ErdosGallai.Lovasz.half_some_none line 1157
  112. lemma OAI.ErdosGallai.Lovasz.option_degree_some line 1161
  113. lemma OAI.ErdosGallai.Lovasz.option_degree_none line 1170
  114. lemma OAI.ErdosGallai.Lovasz.subdivision_old_neighbors line 1178
  115. lemma OAI.ErdosGallai.Lovasz.subdivision_degree line 1195
  116. lemma OAI.ErdosGallai.Lovasz.subdivision_degree_none line 1210
  117. lemma OAI.ErdosGallai.Lovasz.half_degree line 1219
  118. lemma OAI.ErdosGallai.Lovasz.half_degree_none line 1238
  119. lemma OAI.ErdosGallai.Lovasz.subdivision_edge_count line 1247
  120. lemma OAI.ErdosGallai.Lovasz.half_edge_count line 1257
  121. lemma OAI.ErdosGallai.Lovasz.subdivision_activeOrder line 1271
  122. lemma OAI.ErdosGallai.Lovasz.suppress_path line 1290
  123. lemma OAI.ErdosGallai.Lovasz.tight_partition_endpoints line 1367
  124. def OAI.ErdosGallai.Lovasz.subdivisionRepresentative line 1408
  125. lemma OAI.ErdosGallai.Lovasz.representative_mem line 1411
  126. lemma OAI.ErdosGallai.Lovasz.suppress_piece line 1421
  127. lemma OAI.ErdosGallai.Lovasz.suppress_partition line 1455
  128. lemma OAI.ErdosGallai.Lovasz.even_activeOrder line 1478
  129. lemma OAI.ErdosGallai.Lovasz.half_restore line 1490
  130. theorem OAI.ErdosGallai.Lovasz.odd_vertex_step line 1525
  131. theorem OAI.ErdosGallai.Lovasz.path_cycle_partition line 1574