OAI/Combinatorics/CycleDecomposition/BatchLovasz.lean

GitHub source file

131 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ErdosGallai.Batch.Lovasz.StarActive line 20
  2. lemma OAI.ErdosGallai.Batch.Lovasz.starActive_source line 23
  3. lemma OAI.ErdosGallai.Batch.Lovasz.starActive_step line 27
  4. lemma OAI.ErdosGallai.Batch.Lovasz.starActive_iff line 32
  5. lemma OAI.ErdosGallai.Batch.Lovasz.starActive_original_iff line 43
  6. lemma OAI.ErdosGallai.Batch.Lovasz.starActive_subset line 50
  7. lemma OAI.ErdosGallai.Batch.Lovasz.starActive_no_loop line 58
  8. lemma OAI.ErdosGallai.Batch.Lovasz.star_inj line 71
  9. structure OAI.ErdosGallai.Batch.Lovasz.PathPiece line 79
  10. lemma OAI.ErdosGallai.Batch.Lovasz.PathPiece.ends_ne line 86
  11. structure OAI.ErdosGallai.Batch.Lovasz.Piece line 93
  12. def OAI.ErdosGallai.Batch.Lovasz.Piece.ofPath line 103
  13. def OAI.ErdosGallai.Batch.Lovasz.Piece.ofCycle line 106
  14. structure OAI.ErdosGallai.Batch.Lovasz.Arm line 111
  15. def OAI.ErdosGallai.Batch.Lovasz.Arm.tip line 122
  16. def OAI.ErdosGallai.Batch.Lovasz.Arm.flip line 129
  17. lemma OAI.ErdosGallai.Batch.Lovasz.Arm.flip_edges line 137
  18. lemma OAI.ErdosGallai.Batch.Lovasz.Arm.mem_flip_support line 140
  19. lemma OAI.ErdosGallai.Batch.Lovasz.Arm.two_arms_isPath line 143
  20. def OAI.ErdosGallai.Batch.Lovasz.Arm.join line 159
  21. lemma OAI.ErdosGallai.Batch.Lovasz.Arm.join_edges line 166
  22. lemma OAI.ErdosGallai.Batch.Lovasz.Arm.near_ne line 174
  23. lemma OAI.ErdosGallai.Batch.Lovasz.Arm.far_ne line 179
  24. lemma OAI.ErdosGallai.Batch.Lovasz.Arm.far_ne_center line 182
  25. lemma OAI.ErdosGallai.Batch.Lovasz.Arm.star_not_mem line 187
  26. lemma OAI.ErdosGallai.Batch.Lovasz.Arm.flip_disjoint_left line 192
  27. lemma OAI.ErdosGallai.Batch.Lovasz.Arm.flip_disjoint_right line 199
  28. def OAI.ErdosGallai.Batch.Lovasz.Arm.orient line 204
  29. lemma OAI.ErdosGallai.Batch.Lovasz.Arm.orient_edges line 207
  30. lemma OAI.ErdosGallai.Batch.Lovasz.Arm.orient_near line 215
  31. lemma OAI.ErdosGallai.Batch.Lovasz.Arm.mem_orient_support line 219
  32. lemma OAI.ErdosGallai.Batch.Lovasz.Arm.orient_disjoint line 229
  33. inductive OAI.ErdosGallai.Batch.Lovasz.Frame line 240
  34. def OAI.ErdosGallai.Batch.Lovasz.Frame.path line 248
  35. def OAI.ErdosGallai.Batch.Lovasz.Frame.Port line 253
  36. def OAI.ErdosGallai.Batch.Lovasz.Frame.endpoint line 258
  37. def OAI.ErdosGallai.Batch.Lovasz.Frame.exit line 265
  38. def OAI.ErdosGallai.Batch.Lovasz.Frame.inserted line 271
  39. def OAI.ErdosGallai.Batch.Lovasz.Frame.removed line 274
  40. lemma OAI.ErdosGallai.Batch.Lovasz.Frame.endpoint_ne_center line 277
  41. lemma OAI.ErdosGallai.Batch.Lovasz.Frame.endpoint_injective line 288
  42. lemma OAI.ErdosGallai.Batch.Lovasz.Frame.port_iff_endpoint line 302
  43. lemma OAI.ErdosGallai.Batch.Lovasz.Frame.exit_edge line 327
  44. lemma OAI.ErdosGallai.Batch.Lovasz.Frame.removed_subset line 341
  45. lemma OAI.ErdosGallai.Batch.Lovasz.Frame.removed_away line 346
  46. lemma OAI.ErdosGallai.Batch.Lovasz.Frame.removed_tip line 351
  47. lemma OAI.ErdosGallai.Batch.Lovasz.Frame.inserted_away line 355
  48. lemma OAI.ErdosGallai.Batch.Lovasz.Frame.inserted_tip line 364
  49. lemma OAI.ErdosGallai.Batch.Lovasz.Frame.inserted_through line 369
  50. lemma OAI.ErdosGallai.Batch.Lovasz.Frame.removed_through line 378
  51. lemma OAI.ErdosGallai.Batch.Lovasz.replace_two_attachments line 389
  52. lemma OAI.ErdosGallai.Batch.Lovasz.Frame.modify_through line 403
  53. lemma OAI.ErdosGallai.Batch.Lovasz.Frame.modify_tip line 439
  54. lemma OAI.ErdosGallai.Batch.Lovasz.Frame.modify_away line 465
  55. theorem OAI.ErdosGallai.Batch.Lovasz.Frame.modify line 516
  56. theorem OAI.ErdosGallai.Batch.Lovasz.rewire_partition line 528
  57. inductive OAI.ErdosGallai.Batch.Lovasz.Centered line 581
  58. def OAI.ErdosGallai.Batch.Lovasz.Centered.piece line 588
  59. def OAI.ErdosGallai.Batch.Lovasz.Centered.Port line 592
  60. def OAI.ErdosGallai.Batch.Lovasz.Centered.endpoint line 596
  61. def OAI.ErdosGallai.Batch.Lovasz.Centered.exit line 600
  62. def OAI.ErdosGallai.Batch.Lovasz.Centered.inserted line 604
  63. def OAI.ErdosGallai.Batch.Lovasz.Centered.removed line 607
  64. lemma OAI.ErdosGallai.Batch.Lovasz.Centered.exit_edge line 610
  65. lemma OAI.ErdosGallai.Batch.Lovasz.Centered.exit_adj line 616
  66. lemma OAI.ErdosGallai.Batch.Lovasz.Centered.exit_none_all line 620
  67. lemma OAI.ErdosGallai.Batch.Lovasz.Centered.removed_subset line 630
  68. lemma OAI.ErdosGallai.Batch.Lovasz.Centered.modify line 635
  69. theorem OAI.ErdosGallai.Batch.Lovasz.restore_selected line 656
  70. theorem OAI.ErdosGallai.Batch.Lovasz.restore_star line 727
  71. def OAI.ErdosGallai.Batch.Lovasz.Arm.fromWalk line 753
  72. lemma OAI.ErdosGallai.Batch.Lovasz.Arm.fromWalk_far line 760
  73. lemma OAI.ErdosGallai.Batch.Lovasz.Arm.fromWalk_support line 766
  74. lemma OAI.ErdosGallai.Batch.Lovasz.Arm.fromWalk_tip_edges line 772
  75. lemma OAI.ErdosGallai.Batch.Lovasz.PathPiece.exists_frame line 779
  76. lemma OAI.ErdosGallai.Batch.Lovasz.Piece.isTrail line 836
  77. def OAI.ErdosGallai.Batch.Lovasz.Piece.mapLe line 841
  78. lemma OAI.ErdosGallai.Batch.Lovasz.Piece.mapLe_edges line 849
  79. lemma OAI.ErdosGallai.Batch.Lovasz.Piece.mapLe_start line 854
  80. lemma OAI.ErdosGallai.Batch.Lovasz.Piece.mapLe_finish line 856
  81. lemma OAI.ErdosGallai.Batch.Lovasz.Piece.exists_centered line 859
  82. theorem OAI.ErdosGallai.Batch.Lovasz.trail_partition_degree_sum line 875
  83. theorem OAI.ErdosGallai.Batch.Lovasz.trail_partition_even_degree_iff line 904
  84. lemma OAI.ErdosGallai.Batch.Lovasz.endpoint_of_odd line 922
  85. theorem OAI.ErdosGallai.Batch.Lovasz.restore_partition line 941
  86. def OAI.ErdosGallai.Batch.Lovasz.activeOrder line 965
  87. lemma OAI.ErdosGallai.Batch.Lovasz.activeOrder_mono line 968
  88. def OAI.ErdosGallai.Batch.Lovasz.HasPartition line 974
  89. def OAI.ErdosGallai.Batch.Lovasz.evenStarVertices line 979
  90. def OAI.ErdosGallai.Batch.Lovasz.evenStarEdges line 982
  91. def OAI.ErdosGallai.Batch.Lovasz.deleteEvenStar line 985
  92. lemma OAI.ErdosGallai.Batch.Lovasz.evenStar_subset line 988
  93. lemma OAI.ErdosGallai.Batch.Lovasz.deleteEvenStar_neighbor_even line 992
  94. lemma OAI.ErdosGallai.Batch.Lovasz.deleteEvenStar_neighbor_odd line 1012
  95. lemma OAI.ErdosGallai.Batch.Lovasz.deleteEvenStar_neighbor_degree line 1026
  96. lemma OAI.ErdosGallai.Batch.Lovasz.deleteEvenStar_edges line 1040
  97. lemma OAI.ErdosGallai.Batch.Lovasz.deleteEvenStar_fresh line 1045
  98. lemma OAI.ErdosGallai.Batch.Lovasz.deleteEvenStar_lt line 1050
  99. theorem OAI.ErdosGallai.Batch.Lovasz.even_vertex_step line 1066
  100. lemma OAI.ErdosGallai.Batch.Lovasz.single_edge_piece line 1079
  101. lemma OAI.ErdosGallai.Batch.Lovasz.partition_single_edges line 1088
  102. lemma OAI.ErdosGallai.Batch.Lovasz.matching_partition line 1107
  103. def OAI.ErdosGallai.Batch.Lovasz.subdivision line 1116
  104. lemma OAI.ErdosGallai.Batch.Lovasz.subdivision_some line 1135
  105. lemma OAI.ErdosGallai.Batch.Lovasz.subdivision_none_some line 1137
  106. lemma OAI.ErdosGallai.Batch.Lovasz.subdivision_some_none line 1139
  107. lemma OAI.ErdosGallai.Batch.Lovasz.subdivision_none_none line 1141
  108. def OAI.ErdosGallai.Batch.Lovasz.halfSubdivision line 1144
  109. lemma OAI.ErdosGallai.Batch.Lovasz.half_some line 1147
  110. lemma OAI.ErdosGallai.Batch.Lovasz.half_none_some line 1152
  111. lemma OAI.ErdosGallai.Batch.Lovasz.half_some_none line 1158
  112. lemma OAI.ErdosGallai.Batch.Lovasz.option_degree_some line 1162
  113. lemma OAI.ErdosGallai.Batch.Lovasz.option_degree_none line 1171
  114. lemma OAI.ErdosGallai.Batch.Lovasz.subdivision_old_neighbors line 1179
  115. lemma OAI.ErdosGallai.Batch.Lovasz.subdivision_degree line 1196
  116. lemma OAI.ErdosGallai.Batch.Lovasz.subdivision_degree_none line 1211
  117. lemma OAI.ErdosGallai.Batch.Lovasz.half_degree line 1220
  118. lemma OAI.ErdosGallai.Batch.Lovasz.half_degree_none line 1239
  119. lemma OAI.ErdosGallai.Batch.Lovasz.subdivision_edge_count line 1248
  120. lemma OAI.ErdosGallai.Batch.Lovasz.half_edge_count line 1258
  121. lemma OAI.ErdosGallai.Batch.Lovasz.subdivision_activeOrder line 1272
  122. lemma OAI.ErdosGallai.Batch.Lovasz.suppress_path line 1291
  123. lemma OAI.ErdosGallai.Batch.Lovasz.tight_partition_endpoints line 1368
  124. def OAI.ErdosGallai.Batch.Lovasz.subdivisionRepresentative line 1409
  125. lemma OAI.ErdosGallai.Batch.Lovasz.representative_mem line 1412
  126. lemma OAI.ErdosGallai.Batch.Lovasz.suppress_piece line 1422
  127. lemma OAI.ErdosGallai.Batch.Lovasz.suppress_partition line 1456
  128. lemma OAI.ErdosGallai.Batch.Lovasz.even_activeOrder line 1479
  129. lemma OAI.ErdosGallai.Batch.Lovasz.half_restore line 1491
  130. theorem OAI.ErdosGallai.Batch.Lovasz.odd_vertex_step line 1526
  131. theorem OAI.ErdosGallai.Batch.Lovasz.path_cycle_partition line 1575