OAI/Analysis/HardSphere/Geometry/MicroCubeCover.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HardSphere.BathSlice.microCube_cover line 15
2. lemma OAI.HardSphere.BathSlice.lower_corner_mem line 33
3. lemma OAI.HardSphere.BathSlice.step_corner_mem line 40
4. lemma OAI.HardSphere.BathSlice.adjacent_microCubes_inter line 54
5. lemma OAI.HardSphere.BathSlice.exterior_all_liftedBadComponents_good line 66
6. lemma OAI.HardSphere.BathSlice.goodCubes_reach_joined line 73
7. theorem OAI.HardSphere.BathSlice.retained_joined line 87
8. theorem OAI.HardSphere.BathSlice.retained_strict_clearance line 111
9. lemma OAI.HardSphere.BathSlice.isClosed_bad_test line 143
10. lemma OAI.HardSphere.BathSlice.measurableSet_bad_test line 168