OAI/Combinatorics/Hamiltonian/CutSpaces.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Cuts, simplicity, and connectivity of finite oriented networks.

  1. def OAI.Barnette.Network.cut line 12
  2. lemma OAI.Barnette.Network.mem_cut line 16
  3. lemma OAI.Barnette.Network.cut_compl line 20
  4. lemma OAI.Barnette.Network.region_card_le_cut line 25
  5. lemma OAI.Barnette.Network.cut_card_three line 51
  6. lemma OAI.Barnette.Network.gradient_small_support line 64
  7. structure OAI.Barnette.Network.Simple line 95
  8. def OAI.Barnette.Network.basisVec line 99
  9. lemma OAI.Barnette.Network.boundary_basis line 103
  10. theorem OAI.Barnette.Network.Duality.simple_dual line 114
  11. def OAI.Barnette.Network.Incident line 166
  12. lemma OAI.Barnette.Network.incident_iff_mem_pair line 169
  13. lemma OAI.Barnette.Network.pair_eq_of_incident line 175
  14. lemma OAI.Barnette.Network.Simple.incident_other line 184
  15. def OAI.Barnette.Network.flowSupport line 190
  16. lemma OAI.Barnette.Network.mem_flowSupport line 193
  17. lemma OAI.Barnette.Network.flow_no_leaf line 198
  18. structure OAI.Barnette.Network.Triangle line 222
  19. theorem OAI.Barnette.Network.triangle_of_flow line 232