OAI/Analysis/HardSphere/Geometry/SiteCube.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HardSphere.BathSlice.siteCube line 18
2. lemma OAI.HardSphere.BathSlice.siteCube_injective line 21
3. def OAI.HardSphere.BathSlice.siteCubeEmbedding line 29
4. lemma OAI.HardSphere.BathSlice.unitCenter_siteCube line 32
5. lemma OAI.HardSphere.BathSlice.spatial_event_siteCube line 37
6. lemma OAI.HardSphere.BathSlice.IsGroundVector.positionLaw_ae_allowed line 48
7. lemma OAI.HardSphere.BathSlice.allowed_restrict line 63
8. lemma OAI.HardSphere.BathSlice.IsGroundVector.bathLaw_ae_allowed line 70
9. theorem OAI.HardSphere.BathSlice.physical_close_tail line 78
10. theorem OAI.HardSphere.BathSlice.physical_omitted_tail line 104