OAI/Combinatorics/Hamiltonian/ThreeCuts.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Three-edge cuts, capped graphs, and preservation of graph properties.

  1. lemma OAI.Barnette.Network.gradient_small_support_edge line 12
  2. theorem OAI.Barnette.Network.Duality.simple_dual_edge line 37
  3. theorem OAI.Barnette.Network.Duality.cubic_face_triangles_edge line 82
  4. lemma OAI.Barnette.Network.make_coloredDual line 101
  5. lemma OAI.Barnette.Network.irreducible_matching line 109
  6. def OAI.Barnette.Network.capMap line 126
  7. lemma OAI.Barnette.Network.capMap_some line 129
  8. lemma OAI.Barnette.Network.capMap_eq_none line 132
  9. lemma OAI.Barnette.Network.capMap_eq_some line 135
  10. lemma OAI.Barnette.Network.capMap_surjective line 143
  11. abbrev OAI.Barnette.Network.cap line 149
  12. lemma OAI.Barnette.Network.cap_loopless line 153
  13. lemma OAI.Barnette.Network.cap_star_some line 166
  14. lemma OAI.Barnette.Network.cap_star_none line 182
  15. lemma OAI.Barnette.Network.cap_star_card line 199
  16. def OAI.Barnette.Network.capPreimage line 206
  17. lemma OAI.Barnette.Network.mem_capPreimage line 210
  18. lemma OAI.Barnette.Network.cap_cut line 213
  19. lemma OAI.Barnette.Network.cap_threeConnected line 230
  20. lemma OAI.Barnette.Network.ThreeEdgeConnected.connected line 242
  21. lemma OAI.Barnette.Network.threeCut_bond line 258
  22. lemma OAI.Barnette.Network.cap_connectedFibers line 271
  23. lemma OAI.Barnette.Network.simple_of_cubic_stars line 300
  24. lemma OAI.Barnette.Network.cap_simple line 352
  25. lemma OAI.Barnette.Network.cap_cubic line 360
  26. lemma OAI.Barnette.Network.threeCut_black_card line 367
  27. def OAI.Barnette.Network.capBlack line 377
  28. lemma OAI.Barnette.Network.cap_coloring line 381
  29. lemma OAI.Barnette.Network.boundary_range_restrict line 420
  30. lemma OAI.Barnette.Network.exists_independent_restriction line 435
  31. lemma OAI.Barnette.Network.duality_of_first_exact line 451