OAI/Analysis/HardSphere/Geometry/LiftedBadComponent.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.Lattice.liftedBadComponent line 14
  2. def OAI.HardSphere.Lattice.FiniteBadComponents line 17
  3. lemma OAI.HardSphere.Lattice.liftedBadComponent_self line 20
  4. lemma OAI.HardSphere.Lattice.liftedBadComponent_subset line 23
  5. lemma OAI.HardSphere.Lattice.liftedBadComponent_closed line 26
  6. lemma OAI.HardSphere.Lattice.liftedBadComponent_connected line 31
  7. def OAI.HardSphere.Lattice.IsBadComponent line 37
  8. lemma OAI.HardSphere.Lattice.IsBadComponent.connected line 40
  9. lemma OAI.HardSphere.Lattice.IsBadComponent.subset line 46
  10. lemma OAI.HardSphere.Lattice.IsBadComponent.closed line 52
  11. lemma OAI.HardSphere.Lattice.intervalBox_finite line 60
  12. theorem OAI.HardSphere.Lattice.exterior_all_liftedBadComponents_reach line 69
  13. abbrev OAI.HardSphere.BathSlice.Point line 109
  14. def OAI.HardSphere.BathSlice.liftPoint line 111
  15. def OAI.HardSphere.BathSlice.liftedCube line 113
  16. def OAI.HardSphere.BathSlice.microCube line 116
  17. def OAI.HardSphere.BathSlice.forbidden line 119
  18. def OAI.HardSphere.BathSlice.slice line 122
  19. def OAI.HardSphere.BathSlice.bad line 125
  20. def OAI.HardSphere.BathSlice.exceptional line 128
  21. def OAI.HardSphere.BathSlice.omitted line 131
  22. def OAI.HardSphere.BathSlice.retained line 136
  23. lemma OAI.HardSphere.BathSlice.continuous_liftPoint line 139
  24. lemma OAI.HardSphere.BathSlice.isCompact_microCube line 142
  25. lemma OAI.HardSphere.BathSlice.microCube_pathConnected line 146
  26. lemma OAI.HardSphere.BathSlice.goodCube_subset_slice line 154
  27. lemma OAI.HardSphere.BathSlice.retained_finiteComponents line 159
  28. lemma OAI.HardSphere.BathSlice.retained_mem_exterior line 165