OAI/Combinatorics/Hamiltonian/ColoredDual.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Colored dual networks and signed directed state cycles.

  1. structure OAI.Barnette.Network.ColoredDual line 13
  2. abbrev OAI.Barnette.Network.ColoredDual.Black line 27
  3. def OAI.Barnette.Network.ColoredDual.system line 29
  4. def OAI.Barnette.Network.ColoredDual.nonroots line 44
  5. abbrev OAI.Barnette.Network.ColoredDual.State line 46
  6. def OAI.Barnette.Network.ColoredDual.assignment line 48
  7. lemma OAI.Barnette.Network.ColoredDual.assignment_apply line 52
  8. lemma OAI.Barnette.Network.ColoredDual.assignment_inj line 56
  9. lemma OAI.Barnette.Network.ColoredDual.assignment_face line 64
  10. lemma OAI.Barnette.Network.ColoredDual.assignment_range line 71
  11. lemma OAI.Barnette.Network.ColoredDual.cycle_disk line 83
  12. def OAI.Barnette.Network.ColoredDual.weights line 102
  13. lemma OAI.Barnette.Network.ColoredDual.weights_diff line 106
  14. structure OAI.Barnette.Network.ColoredDual.StateCycle line 126
  15. lemma OAI.Barnette.Network.ColoredDual.StateCycle.corner_ne line 137
  16. lemma OAI.Barnette.Network.ColoredDual.StateCycle.cycleEdge_eq line 144
  17. lemma OAI.Barnette.Network.ColoredDual.StateCycle.edge_mem line 153
  18. def OAI.Barnette.Network.ColoredDual.StateCycle.delta line 157
  19. def OAI.Barnette.Network.ColoredDual.StateCycle.slope line 159
  20. lemma OAI.Barnette.Network.ColoredDual.StateCycle.delta_eq line 163
  21. lemma OAI.Barnette.Network.ColoredDual.StateCycle.slope_eq line 173
  22. theorem OAI.Barnette.Network.ColoredDual.StateCycle.signed line 183