OAI/Combinatorics/Hamiltonian/Bonds.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Cycle flows, minimal cuts, and connected shores.

  1. def OAI.Barnette.Network.arcSign line 14
  2. lemma OAI.Barnette.Network.arcSign_ne_zero line 17
  3. lemma OAI.Barnette.Network.boundary_directed_unit line 21
  4. def OAI.Barnette.Network.cycleFlow line 37
  5. lemma OAI.Barnette.Network.cycleFlow_conserved line 41
  6. lemma OAI.Barnette.Network.cycleFlow_apply_edge line 54
  7. lemma OAI.Barnette.Network.cycleFlow_zero_outside line 65
  8. lemma OAI.Barnette.Network.cycleFlow_support line 74
  9. lemma OAI.Barnette.Network.cycleFlow_circuit line 86
  10. lemma OAI.Barnette.Network.support_cut line 98
  11. structure OAI.Barnette.Network.Bond line 104
  12. lemma OAI.Barnette.Network.Duality.bond_of_circuit line 109
  13. lemma OAI.Barnette.Network.cuts_equal_subset line 127
  14. lemma OAI.Barnette.Network.cut_nonempty line 149
  15. lemma OAI.Barnette.Network.Bond.connected_shore line 163
  16. lemma OAI.Barnette.Network.Bond.compl line 200
  17. lemma OAI.Barnette.Network.Triangle.corner_iff_incident line 215
  18. lemma OAI.Barnette.Network.Triangle.clique line 232
  19. lemma OAI.Barnette.Network.Triangle.corner_avoiding line 242
  20. lemma OAI.Barnette.Network.Triangle.reachable_avoiding line 252
  21. theorem OAI.Barnette.Network.faces_vertex_deleted_connected line 265