OAI/Analysis/HardSphere/Geometry/PathSlots.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HardSphere.Comparison.pathVertexEmbedding line 16
2. lemma OAI.HardSphere.Comparison.pathVertex_zero line 23
3. lemma OAI.HardSphere.Comparison.pathVertex_last line 25
4. def OAI.HardSphere.Comparison.departureEmbedding line 28
5. def OAI.HardSphere.Comparison.extendedAnchor line 38
6. lemma OAI.HardSphere.Comparison.routeEmbedding_anchor line 41
7. lemma OAI.HardSphere.Comparison.routeSlots_anchor_injective line 55
8. lemma OAI.HardSphere.Comparison.routeSlots_sites line 65
9. lemma OAI.HardSphere.Comparison.simple_nearSlots_bound line 83