OAI/Combinatorics/ListHadwiger/EggCover.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ReedSeymour.loops_even_of_cycles_even line 10
  2. lemma OAI.ReedSeymour.two_colorable_of_cycles_even line 51
  3. def OAI.ReedSeymour.Shortest line 56
  4. lemma OAI.ReedSeymour.exists_shortest line 59
  5. lemma OAI.ReedSeymour.Shortest.separated line 66
  6. lemma OAI.ReedSeymour.Shortest.adj_indices line 76
  7. def OAI.ReedSeymour.ReachOn line 91
  8. lemma OAI.ReedSeymour.ReachOn.left line 94
  9. lemma OAI.ReedSeymour.ReachOn.right line 96
  10. lemma OAI.ReedSeymour.ReachOn.refl line 98
  11. lemma OAI.ReedSeymour.ReachOn.symm line 100
  12. lemma OAI.ReedSeymour.ReachOn.trans line 103
  13. lemma OAI.ReedSeymour.ReachOn.mono line 109
  14. lemma OAI.ReedSeymour.ReachOn.adj line 113
  15. lemma OAI.ReedSeymour.connected_iff_reachOn line 117
  16. lemma OAI.ReedSeymour.connected_reachOn line 136
  17. def OAI.ReedSeymour.component line 140
  18. lemma OAI.ReedSeymour.component_subset line 143
  19. lemma OAI.ReedSeymour.component_connected line 146
  20. lemma OAI.ReedSeymour.cycle_delete_connected_root line 157
  21. lemma OAI.ReedSeymour.cycle_delete_connected line 178
  22. structure OAI.ReedSeymour.BetweenMin line 187
  23. lemma OAI.ReedSeymour.exists_betweenMin line 192
  24. lemma OAI.ReedSeymour.BetweenMin.shortest line 206
  25. lemma OAI.ReedSeymour.BetweenMin.source_only line 210
  26. lemma OAI.ReedSeymour.BetweenMin.target_only line 218
  27. lemma OAI.ReedSeymour.Shortest.isPath line 226
  28. structure OAI.ReedSeymour.MinimalConnector line 231
  29. def OAI.ReedSeymour.Gate line 237
  30. lemma OAI.ReedSeymour.MinimalConnector.cycle_gate line 240
  31. lemma OAI.ReedSeymour.Gate.mem_support line 260
  32. structure OAI.ReedSeymour.Tail line 265
  33. lemma OAI.ReedSeymour.exists_tail line 272
  34. lemma OAI.ReedSeymour.Tail.avoid line 282
  35. lemma OAI.ReedSeymour.Tail.index_ne line 286
  36. lemma OAI.ReedSeymour.Tail.disjoint line 293
  37. lemma OAI.ReedSeymour.Tail.cross_edges line 309
  38. lemma OAI.ReedSeymour.Tail.interface_avoid line 330
  39. structure OAI.ReedSeymour.SplitConnector line 338
  40. def OAI.ReedSeymour.parity line 351
  41. lemma OAI.ReedSeymour.parity_adj line 353
  42. lemma OAI.ReedSeymour.parity_add_one line 359
  43. lemma OAI.ReedSeymour.Shortest.idxOf_getVert line 366
  44. lemma OAI.ReedSeymour.Shortest.idxOf_endpoint line 371
  45. lemma OAI.ReedSeymour.Shortest.idxOf_start line 375
  46. lemma OAI.ReedSeymour.Shortest.parity_proper line 379
  47. lemma OAI.ReedSeymour.connected_union_of_adj line 396
  48. lemma OAI.ReedSeymour.tails_split line 407
  49. lemma OAI.ReedSeymour.MinimalConnector.two_colorable_or_split line 461
  50. def OAI.ReedSeymour.extendColor line 484
  51. lemma OAI.ReedSeymour.extendColor_apply line 488
  52. lemma OAI.ReedSeymour.colorable_induce_iff_total line 491
  53. lemma OAI.ReedSeymour.connected_image_val line 501
  54. lemma OAI.ReedSeymour.colorable_image_val line 514
  55. def OAI.ReedSeymour.SplitConnector.lift line 524
  56. lemma OAI.ReedSeymour.SplitConnector.lift_subset line 550
  57. lemma OAI.ReedSeymour.exists_minimal_transversal line 556
  58. lemma OAI.ReedSeymour.connected_transversal_or_split line 605
  59. lemma OAI.ReedSeymour.connected_transversal_or_split_on line 614
  60. def OAI.ReedSeymour.Touch line 635
  61. lemma OAI.ReedSeymour.Touch.symm line 638
  62. lemma OAI.ReedSeymour.Touch.mono line 642
  63. lemma OAI.ReedSeymour.Touch.left_nonempty line 647
  64. lemma OAI.ReedSeymour.Touch.right_nonempty line 651
  65. lemma OAI.ReedSeymour.touch_union_left line 653
  66. lemma OAI.ReedSeymour.touch_union_right line 661
  67. lemma OAI.ReedSeymour.connected_union_of_touch line 669
  68. def OAI.ReedSeymour.Independent line 674
  69. lemma OAI.ReedSeymour.independent_empty line 677
  70. lemma OAI.ReedSeymour.Independent.mono line 679
  71. lemma OAI.ReedSeymour.independent_union line 682