OAI/MathematicalPhysics/Heisenberg/LatticePaths.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Heisenberg.Geometry.reach_rectangle line 10
  2. lemma OAI.Heisenberg.Geometry.shell_to_corner line 41
  3. lemma OAI.Heisenberg.Geometry.shell_connected line 92
  4. abbrev OAI.Heisenberg.Geometry.Direction line 98
  5. def OAI.Heisenberg.Geometry.Ray line 100
  6. lemma OAI.Heisenberg.Geometry.ray_unique line 104
  7. lemma OAI.Heisenberg.Geometry.exists_clear_ray line 121
  8. lemma OAI.Heisenberg.Geometry.shell_radius_unique line 136
  9. lemma OAI.Heisenberg.Geometry.exists_clean_shell line 142
  10. lemma OAI.Heisenberg.Geometry.reach_shell line 165
  11. lemma OAI.Heisenberg.Geometry.box_mono line 219
  12. theorem OAI.Heisenberg.Geometry.finite_obstacle_connection line 222
  13. def OAI.Heisenberg.Geometry.latticeGraph line 238
  14. lemma OAI.Heisenberg.Geometry.reach_has_simple_path line 246
  15. def OAI.Heisenberg.Geometry.boxFinset line 251
  16. lemma OAI.Heisenberg.Geometry.mem_boxFinset line 254
  17. lemma OAI.Heisenberg.Geometry.card_boxFinset line 258
  18. lemma OAI.Heisenberg.Geometry.path_support_mem line 263
  19. lemma OAI.Heisenberg.Geometry.simple_path_length_bound line 274