OAI/Combinatorics/Hamiltonian/Network.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Oriented finite networks, cycle and cut spaces, and graph realization.

  1. structure OAI.Barnette.Network line 9
  2. def OAI.Barnette.Network.graph line 17
  3. theorem OAI.Barnette.Network.edge_reachable line 23
  4. def OAI.Barnette.Network.gradient line 29
  5. theorem OAI.Barnette.Network.gradient_apply line 34
  6. theorem OAI.Barnette.Network.gradient_const line 37
  7. theorem OAI.Barnette.Network.gradient_eq_zero_iff line 40
  8. theorem OAI.Barnette.Network.gradient_zero_adj line 44
  9. theorem OAI.Barnette.Network.gradient_zero_reachable line 50
  10. def OAI.Barnette.Network.constant line 57
  11. theorem OAI.Barnette.Network.ker_gradient line 62
  12. def OAI.Barnette.Network.incidence line 78
  13. def OAI.Barnette.Network.boundary line 81
  14. theorem OAI.Barnette.Network.boundary_apply line 84
  15. theorem OAI.Barnette.Network.gradient_matrix line 92
  16. theorem OAI.Barnette.Network.sum_boundary line 100
  17. theorem OAI.Barnette.Network.rank_gradient line 107
  18. theorem OAI.Barnette.Network.rank_boundary line 119
  19. theorem OAI.Barnette.Network.dim_cycles line 127
  20. theorem OAI.Barnette.Network.boundary_adjoint line 134
  21. theorem OAI.Barnette.Network.orthogonal_symm line 145
  22. structure OAI.Barnette.Network.Duality line 164
  23. theorem OAI.Barnette.Network.ker_eq_range_of_orth_card line 170
  24. theorem OAI.Barnette.Network.duality_of_orth_card line 182
  25. theorem OAI.Barnette.Network.Duality.euler line 192
  26. lemma OAI.Barnette.cubic_bipartite_order line 210
  27. lemma OAI.Barnette.boundary_cover_of_threeConnected line 241