OAI/Combinatorics/Hamiltonian/TriangleSystem.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Triangle incidence states, opposite graphs, and oriented potentials.

  1. structure OAI.Barnette.TriangleSystem line 9
  2. def OAI.Barnette.TriangleSystem.State line 19
  3. def OAI.Barnette.TriangleSystem.State.value line 27
  4. theorem OAI.Barnette.TriangleSystem.State.value_injective line 29
  5. theorem OAI.Barnette.TriangleSystem.State.value_range line 31
  6. theorem OAI.Barnette.TriangleSystem.State.value_mem line 33
  7. def OAI.Barnette.TriangleSystem.State.toEquiv line 36
  8. theorem OAI.Barnette.TriangleSystem.State.coe_toEquiv line 44
  9. theorem OAI.Barnette.TriangleSystem.State.value_eq_iff line 46
  10. theorem OAI.Barnette.TriangleSystem.State.ext line 49
  11. instance OAI.Barnette.TriangleSystem.State.(instance at line 54) line 54
  12. instance OAI.Barnette.TriangleSystem.State.(instance at line 56) line 56
  13. theorem OAI.Barnette.TriangleSystem.state_nonempty_iff line 60
  14. def OAI.Barnette.TriangleSystem.Partner line 82
  15. def OAI.Barnette.TriangleSystem.thirdIndex line 84
  16. theorem OAI.Barnette.TriangleSystem.thirdIndex_distinct line 86
  17. theorem OAI.Barnette.TriangleSystem.thirdIndex_involution line 89
  18. theorem OAI.Barnette.TriangleSystem.other_corners line 92
  19. def OAI.Barnette.TriangleSystem.indexDelta line 96
  20. theorem OAI.Barnette.TriangleSystem.indexDelta_antisymm line 98
  21. theorem OAI.Barnette.TriangleSystem.indexDelta_third line 101
  22. def OAI.Barnette.TriangleSystem.oppositeGraph line 105
  23. theorem OAI.Barnette.TriangleSystem.oppositeGraph_adj_iff line 113
  24. lemma OAI.Barnette.Network.Triangle.oriented_cycleFlow line 145
  25. lemma OAI.Barnette.Network.cycle_integral line 169
  26. lemma OAI.Barnette.Network.Triangle.oriented_integral line 179
  27. def OAI.Barnette.Network.Triangle.potential line 194
  28. lemma OAI.Barnette.Network.Triangle.potential_step line 200
  29. def OAI.Barnette.Network.Triangle.side line 221
  30. lemma OAI.Barnette.Network.Triangle.side_mem line 225
  31. lemma OAI.Barnette.Network.Triangle.side_ends line 234
  32. lemma OAI.Barnette.Network.Triangle.side_unique line 247
  33. lemma OAI.Barnette.Network.Triangle.potential_side line 253
  34. lemma OAI.Barnette.Network.blackGradient_face line 276
  35. lemma OAI.Barnette.Network.Triangle.index_delta line 291