OAI/Combinatorics/Hamiltonian/Contraction.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Contraction and deletion of finite oriented dual networks.

  1. def OAI.Barnette.Network.inducedEdges line 13
  2. lemma OAI.Barnette.Network.mem_inducedEdges line 17
  3. def OAI.Barnette.Network.inducedNetwork line 21
  4. lemma OAI.Barnette.Network.inducedNetwork_map line 26
  5. lemma OAI.Barnette.Network.inducedNetwork_boundary line 30
  6. def OAI.Barnette.Network.regions line 35
  7. abbrev OAI.Barnette.Network.Regions line 38
  8. def OAI.Barnette.Network.regionQuotient line 40
  9. lemma OAI.Barnette.Network.regionQuotient_connected line 44
  10. lemma OAI.Barnette.Network.induced_cycles_eq_regions line 63
  11. lemma OAI.Barnette.Network.rank_boundary_le line 103
  12. lemma OAI.Barnette.Network.induced_euler_bound line 121
  13. lemma OAI.Barnette.Network.star_count line 141
  14. lemma OAI.Barnette.Network.weighted_stars line 150
  15. def OAI.Barnette.Network.colorSign line 159
  16. lemma OAI.Barnette.Network.colorSign_add line 162
  17. lemma OAI.Barnette.Network.colorSign_sum line 169
  18. def OAI.Barnette.Network.regionShore line 178
  19. lemma OAI.Barnette.Network.mem_regionShore line 182
  20. lemma OAI.Barnette.Network.regionShore_nonempty line 187
  21. lemma OAI.Barnette.Network.regionShore_off_edge line 193
  22. def OAI.Barnette.Network.rim line 202
  23. def OAI.Barnette.Network.blackRim line 206
  24. def OAI.Barnette.Network.regionBalance line 210
  25. lemma OAI.Barnette.Network.blackRim_le line 214
  26. lemma OAI.Barnette.Network.region_balance_rim line 223
  27. lemma OAI.Barnette.Network.sum_rim line 258
  28. lemma OAI.Barnette.Network.sum_regionBalance line 265
  29. lemma OAI.Barnette.Network.rim_defect line 273
  30. def OAI.Barnette.Network.ThreeEdgeConnected line 291
  31. def OAI.Barnette.Network.TrivialThreeCuts line 293
  32. lemma OAI.Barnette.Network.region_cut_subset line 296
  33. lemma OAI.Barnette.Network.rim_cut_count line 305
  34. lemma OAI.Barnette.Network.cut_le_rim line 322
  35. lemma OAI.Barnette.Network.rim_of_shore_univ line 328
  36. lemma OAI.Barnette.Network.rim_ge_three line 334
  37. lemma OAI.Barnette.Network.rim_three_cut line 346
  38. lemma OAI.Barnette.Network.rim_three_no_internal line 362
  39. lemma OAI.Barnette.Network.singleton_region_star line 379
  40. lemma OAI.Barnette.Network.star_subset_eq line 390
  41. lemma OAI.Barnette.Network.complement_singleton_root line 407