OAI/Probability/LatticeSurface/Geometry/TriangularCover.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.TriangularLipschitz.Vertex line 11
  2. def OAI.TriangularLipschitz.Adj line 13
  3. def OAI.TriangularLipschitz.boxIndex line 18
  4. def OAI.TriangularLipschitz.centralBox line 20
  5. lemma OAI.TriangularLipschitz.centralBox_card line 23
  6. lemma OAI.TriangularLipschitz.boxIndex_mem line 27
  7. lemma OAI.TriangularLipschitz.ediv_neighbor line 38
  8. lemma OAI.TriangularLipschitz.adj_boxIndex line 58
  9. def OAI.TriangularLipschitz.boxNeighborSet line 68
  10. lemma OAI.TriangularLipschitz.boxNeighborSet_card line 71
  11. lemma OAI.TriangularLipschitz.mem_boxNeighborSet line 78
  12. def OAI.TriangularLipschitz.boxSet line 85
  13. abbrev OAI.TriangularLipschitz.Boxes line 88
  14. def OAI.TriangularLipschitz.boxMap line 90
  15. def OAI.TriangularLipschitz.coverGraph line 93
  16. lemma OAI.TriangularLipschitz.boxMap_adjacent line 103
  17. lemma OAI.TriangularLipschitz.boxMap_fiber line 112
  18. def OAI.TriangularLipschitz.coverNeighbors line 124
  19. lemma OAI.TriangularLipschitz.coverGraph_degree line 130
  20. def OAI.TriangularLipschitz.steps line 139
  21. lemma OAI.TriangularLipschitz.steps_card line 141
  22. lemma OAI.TriangularLipschitz.adj_iff_steps line 143
  23. lemma OAI.TriangularLipschitz.finite_graph_degree line 150