OAI/Analysis/HardSphere/Paths/SimpleRouteGeometry.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.Groups.simpleRouteVertices line 18
  2. lemma OAI.HardSphere.Groups.simpleRouteVertices_zero line 21
  3. lemma OAI.HardSphere.Groups.simpleRouteVertices_last line 23
  4. lemma OAI.HardSphere.Groups.simpleRouteVertices_adjacent line 28
  5. lemma OAI.HardSphere.Groups.simpleRouteVertices_distance line 33
  6. def OAI.HardSphere.Groups.simpleRouteSteps line 39
  7. lemma OAI.HardSphere.Groups.simpleRouteSteps_period line 43
  8. lemma OAI.HardSphere.Groups.gridSite_slotCenter line 49
  9. lemma OAI.HardSphere.Groups.routeSlots_reparam line 57
  10. lemma OAI.HardSphere.Groups.simpleRouteSlots line 62
  11. lemma OAI.HardSphere.Groups.simpleRoute_near_first line 78
  12. lemma OAI.HardSphere.Groups.simpleRoute_near_second line 90