OAI/Combinatorics/Hamiltonian/Rectangle.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Rectangular primal and dual networks and finite lattice containment.

  1. abbrev OAI.Barnette.RectangularDual.Vertex line 10
  2. abbrev OAI.Barnette.RectangularDual.Edge line 11
  3. abbrev OAI.Barnette.RectangularDual.Face line 12
  4. def OAI.Barnette.RectangularDual.primal line 14
  5. def OAI.Barnette.RectangularDual.lower line 18
  6. def OAI.Barnette.RectangularDual.upper line 19
  7. def OAI.Barnette.RectangularDual.dual line 21
  8. def OAI.Barnette.RectangularDual.lowerValue line 29
  9. def OAI.Barnette.RectangularDual.upperValue line 30
  10. def OAI.Barnette.RectangularDual.stepCoeff line 32
  11. lemma OAI.Barnette.RectangularDual.sum_succ line 35
  12. lemma OAI.Barnette.RectangularDual.sum_castSucc line 41
  13. lemma OAI.Barnette.RectangularDual.sum_stepCoeff line 47
  14. lemma OAI.Barnette.RectangularDual.lower_eval line 52
  15. lemma OAI.Barnette.RectangularDual.upper_eval line 56
  16. def OAI.Barnette.RectangularDual.potential line 60
  17. lemma OAI.Barnette.RectangularDual.eval_map line 63
  18. lemma OAI.Barnette.RectangularDual.dual_horizontal line 66
  19. lemma OAI.Barnette.RectangularDual.dual_vertical line 75
  20. lemma OAI.Barnette.RectangularDual.boundary_formula line 83
  21. lemma OAI.Barnette.RectangularDual.orthogonal_potential line 95
  22. lemma OAI.Barnette.RectangularDual.orthogonal line 112
  23. lemma OAI.Barnette.RectangularDual.horizontal_adj line 121
  24. lemma OAI.Barnette.RectangularDual.vertical_adj line 129
  25. lemma OAI.Barnette.RectangularDual.primal_connected line 137
  26. lemma OAI.Barnette.RectangularDual.dual_connected line 151
  27. theorem OAI.Barnette.RectangularDual.grid_duality line 180
  28. def OAI.Barnette.MinorModel.pullHost line 197
  29. lemma OAI.Barnette.RectangularDual.primal_adj_iff line 229
  30. def OAI.Barnette.RectangularDual.latticePoint line 261
  31. lemma OAI.Barnette.RectangularDual.latticePoint_injective line 264
  32. def OAI.Barnette.RectangularDual.latticeEmbedding line 271
  33. lemma OAI.Barnette.RectangularDual.bounded_mem_range line 281
  34. lemma OAI.Barnette.RectangularDual.finite_subset_box line 293
  35. theorem OAI.Barnette.RectangularDual.lattice_minor_in_rectangle line 303