OAI/Combinatorics/Hamiltonian/MinorModel.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Clean finite walks, disjoint grown branches, and lattice minors.

  1. structure OAI.Barnette.MinorModel line 11
  2. theorem OAI.Barnette.WalkSelection.shortest_join line 22
  3. structure OAI.Barnette.WalkSelection.CleanConnection line 51
  4. theorem OAI.Barnette.WalkSelection.exists_clean_connection line 62
  5. def OAI.Barnette.WalkSelection.CleanConnection.leftSet line 101
  6. theorem OAI.Barnette.WalkSelection.CleanConnection.leftSet_finite line 103
  7. theorem OAI.Barnette.WalkSelection.CleanConnection.leftSet_connected line 105
  8. theorem OAI.Barnette.WalkSelection.CleanConnection.start_mem_leftSet line 108
  9. theorem OAI.Barnette.WalkSelection.CleanConnection.leftSet_subset line 110
  10. theorem OAI.Barnette.WalkSelection.CleanConnection.leftSet_disjoint_finish line 115
  11. theorem OAI.Barnette.WalkSelection.CleanConnection.leftSet_adj_finish line 131
  12. theorem OAI.Barnette.CorridorModel.exists_edgeDart line 151
  13. def OAI.Barnette.CorridorModel.edgeDart line 156
  14. theorem OAI.Barnette.CorridorModel.edgeDart_edge line 158
  15. def OAI.Barnette.CorridorModel.connection line 163
  16. def OAI.Barnette.CorridorModel.extension line 168
  17. theorem OAI.Barnette.CorridorModel.extension_finite line 170
  18. theorem OAI.Barnette.CorridorModel.extension_connected line 173
  19. theorem OAI.Barnette.CorridorModel.extension_subset line 176
  20. theorem OAI.Barnette.CorridorModel.extension_disjoint_branch line 179
  21. theorem OAI.Barnette.CorridorModel.extensions_disjoint line 187
  22. def OAI.Barnette.CorridorModel.grownBranch line 193
  23. theorem OAI.Barnette.CorridorModel.branch_subset_grown line 196
  24. theorem OAI.Barnette.CorridorModel.extension_subset_grown line 199
  25. theorem OAI.Barnette.CorridorModel.grownBranch_connected line 202
  26. theorem OAI.Barnette.CorridorModel.grownBranches_disjoint line 219
  27. theorem OAI.Barnette.CorridorModel.grownBranch_adjacency line 237
  28. theorem OAI.Barnette.CorridorModel.grownBranch_finite line 252
  29. def OAI.Barnette.CorridorModel.toMinorModel line 256
  30. theorem OAI.Barnette.PlaneEmbedding.exists_lattice_minor_model line 271