OAI/Combinatorics/Hamiltonian/FlowCircuits.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Minimal flow circuits, triangular faces, and simple cycle coordinates.

  1. structure OAI.Barnette.Network.FlowCircuit line 13
  2. lemma OAI.Barnette.Network.flowSupport_eq_empty_iff line 20
  3. lemma OAI.Barnette.Network.Duality.dual_conserved_gradient line 25
  4. lemma OAI.Barnette.Network.Duality.gradient_of_dual_conserved line 31
  5. theorem OAI.Barnette.Network.Duality.circuit_two_levels line 38
  6. theorem OAI.Barnette.Network.Duality.circuit_cut line 71
  7. def OAI.Barnette.Network.star line 134
  8. lemma OAI.Barnette.Network.mem_star line 137
  9. def OAI.Barnette.Network.otherEnd line 141
  10. lemma OAI.Barnette.Network.otherEnd_spec line 144
  11. lemma OAI.Barnette.Network.otherEnd_adj line 155
  12. lemma OAI.Barnette.Network.card_star line 160
  13. lemma OAI.Barnette.Network.gradient_indicator_support line 185
  14. theorem OAI.Barnette.Network.Duality.cubic_face_triangles line 194
  15. theorem OAI.Barnette.cyclic_propagation line 210
  16. theorem OAI.Barnette.cyclic_one_ne_zero line 222
  17. theorem OAI.Barnette.cyclic_two_ne_zero line 227
  18. structure OAI.Barnette.CycleCoordinates line 232
  19. theorem OAI.Barnette.CycleCoordinates.edge_indices_unique line 241
  20. theorem OAI.Barnette.CycleCoordinates.tail_orientation line 255
  21. def OAI.Barnette.Network.cycleEdge line 287
  22. lemma OAI.Barnette.Network.cycleEdge_ends line 290
  23. lemma OAI.Barnette.Network.cycleEdge_injective line 295
  24. lemma OAI.Barnette.Network.cycleEdge_incident line 302
  25. def OAI.Barnette.Network.cycleEdges line 308
  26. lemma OAI.Barnette.Network.mem_cycleEdges line 311
  27. lemma OAI.Barnette.Network.cycle_support_minimal line 316
  28. lemma OAI.Barnette.Network.flowCircuit_of_cycle line 342