OAI/Combinatorics/Hamiltonian/Quotients.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Vertex quotients and connected fibers of incidence networks.

  1. def OAI.Barnette.Network.push line 12
  2. def OAI.Barnette.Network.pull line 25
  3. theorem OAI.Barnette.Network.pull_apply line 28
  4. theorem OAI.Barnette.Network.push_apply line 31
  5. def OAI.Barnette.Network.mapVertices line 34
  6. def OAI.Barnette.Network.restrict line 37
  7. theorem OAI.Barnette.Network.gradient_mapVertices line 40
  8. theorem OAI.Barnette.Network.gradient_restrict line 43
  9. lemma OAI.Barnette.Network.push_adjoint line 48
  10. lemma OAI.Barnette.Network.push_surjective line 55
  11. lemma OAI.Barnette.Network.pull_injective line 75
  12. lemma OAI.Barnette.Network.eq_of_dot_eq line 82
  13. lemma OAI.Barnette.Network.boundary_mapVertices line 89
  14. lemma OAI.Barnette.Network.boundary_restrict line 96
  15. lemma OAI.Barnette.Network.pull_push_injective line 104
  16. lemma OAI.Barnette.Network.push_eq_zero_outside line 111
  17. lemma OAI.Barnette.Network.push_pull_subtype line 119
  18. def OAI.Barnette.Network.internal line 130
  19. lemma OAI.Barnette.Network.push_boundary_internal line 133
  20. def OAI.Barnette.Network.ConnectedFibers line 148
  21. lemma OAI.Barnette.Network.ker_internal_gradient line 152
  22. lemma OAI.Barnette.Network.range_internal_boundary line 169