OAI/Analysis/HardSphere/Geometry/EndpointsExterior.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HardSphere.Lattice.bad_reachable_induce line 12
2. lemma OAI.HardSphere.Lattice.periodicLift_internalReach line 24
3. lemma OAI.HardSphere.Lattice.exists_bad_lift line 33
4. def OAI.HardSphere.Lattice.endpointsExterior line 66
5. lemma OAI.HardSphere.Lattice.torusRangeGraph_mono line 72
6. lemma OAI.HardSphere.Lattice.badGraph_graphMono line 77
7. def OAI.HardSphere.Lattice.torusNearestGraph line 82
8. def OAI.HardSphere.Lattice.nearestProjection line 90
9. theorem OAI.HardSphere.Lattice.periodic_good_detour line 96