OAI/Combinatorics/Hamiltonian/CappedDuality.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Exact duals of capped graphs and Hamiltonian walks in degree-two graphs.

  1. lemma OAI.Barnette.Network.push_pull_injective line 15
  2. lemma OAI.Barnette.Network.pull_push_disjoint line 26
  3. lemma OAI.Barnette.Network.split_support line 32
  4. lemma OAI.Barnette.Network.push_boundary_on_internal line 47
  5. theorem OAI.Barnette.Network.Duality.minor line 62
  6. lemma OAI.Barnette.Network.cap_duality line 148
  7. lemma OAI.Barnette.Network.cap_card_lt line 162
  8. lemma OAI.Barnette.Network.nontrivial_threeCut line 167
  9. lemma OAI.Barnette.SimpleCycle.cycle_at_of_connected_two line 187
  10. lemma OAI.Barnette.SimpleCycle.induced_support_connected line 213
  11. lemma OAI.Barnette.SimpleCycle.delete_vertex_connected line 223