OAI/Combinatorics/Hamiltonian/ExactDual.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Graph realization and exact finite duality for topological plane embeddings.

  1. def OAI.Barnette.Network.Realizes line 12
  2. lemma OAI.Barnette.Network.Realizes.graph_eq line 16
  3. lemma OAI.Barnette.Network.Realizes.loopless line 31
  4. lemma OAI.Barnette.Network.exists_dart_for_edge line 37
  5. lemma OAI.Barnette.Network.connectedFibers_of_partition line 44
  6. theorem OAI.Barnette.Network.minor_quotient line 69
  7. theorem OAI.Barnette.Network.Duality.graphMinor line 96
  8. theorem OAI.Barnette.PlaneEmbedding.exists_exact_dual line 116