OAI/Combinatorics/Hamiltonian/Circulation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Oriented triangular faces and positive white-face charges.

  1. lemma OAI.Barnette.Network.FlowCircuit.proportional line 15
  2. def OAI.Barnette.Network.Triangle.coordinates line 42
  3. lemma OAI.Barnette.Network.Triangle.coordinates_edge line 51
  4. lemma OAI.Barnette.Network.Triangle.coordinates_edges line 57
  5. def OAI.Barnette.Network.Triangle.reverse line 65
  6. lemma OAI.Barnette.Network.arcSign_opposite line 91
  7. theorem OAI.Barnette.Network.oriented_face line 100
  8. lemma OAI.Barnette.Network.boundary_of_sum_zero line 154
  9. def OAI.Barnette.Network.whiteCharge line 183
  10. lemma OAI.Barnette.Network.whiteCharge_sum line 187
  11. lemma OAI.Barnette.Network.whiteCharge_black line 194
  12. lemma OAI.Barnette.Network.whiteCharge_inside line 198
  13. lemma OAI.Barnette.Network.whiteCharge_cut_integral line 208
  14. lemma OAI.Barnette.Network.white_positive_of_boundary line 227