OAI/Analysis/HardSphere/Geometry/GridAlignment.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.Groups.gridCube line 18
  2. lemma OAI.HardSphere.Groups.gridCube_injective line 19
  3. def OAI.HardSphere.Groups.gridSite line 27
  4. lemma OAI.HardSphere.Groups.gridSite_injective line 28
  5. lemma OAI.HardSphere.Groups.siteCube_gridSite line 35
  6. def OAI.HardSphere.Groups.gridShift line 43
  7. lemma OAI.HardSphere.Groups.shifted_unitCenter line 45
  8. lemma OAI.HardSphere.Groups.shifted_siteCenter line 56
  9. lemma OAI.HardSphere.Groups.grid_visitorCount line 61
  10. def OAI.HardSphere.Groups.rangePackingBox line 81
  11. lemma OAI.HardSphere.Groups.card_rangePackingBox line 83
  12. lemma OAI.HardSphere.Groups.grid_packing_witness line 89
  13. lemma OAI.HardSphere.Groups.card_near_grid_le line 115
  14. lemma OAI.HardSphere.Groups.card_near_labels line 131