OAI/Analysis/HardSphere/Allocation/PhysicalDatum.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.HardSphere.Groups.PhysicalDatum line 17
  2. def OAI.HardSphere.Groups.physicalDatum line 21
  3. lemma OAI.HardSphere.Groups.physicalDatum_measurable line 28
  4. def OAI.HardSphere.Groups.physicalDatumLaw line 55
  5. lemma OAI.HardSphere.Groups.physicalDatumLaw_probability line 62
  6. def OAI.HardSphere.Groups.datumSelected line 70
  7. def OAI.HardSphere.Groups.datumHome line 73
  8. def OAI.HardSphere.Groups.anchorPoint line 76
  9. lemma OAI.HardSphere.Groups.anchorPoint_project line 78
  10. def OAI.HardSphere.Groups.datumStart line 81
  11. def OAI.HardSphere.Groups.datumEnd line 85
  12. lemma OAI.HardSphere.Groups.datumHome_measurable line 89
  13. lemma OAI.HardSphere.Groups.datumAnchor_measurable line 93
  14. lemma OAI.HardSphere.Groups.nearestLift_measurable line 97
  15. lemma OAI.HardSphere.Groups.datumStart_measurable line 106
  16. lemma OAI.HardSphere.Groups.datumEnd_measurable line 112
  17. lemma OAI.HardSphere.Groups.datumFrozen_measurable line 118
  18. lemma OAI.HardSphere.Groups.datumFrozen_collision_measurable line 124
  19. def OAI.HardSphere.Groups.datumPermitted line 136
  20. lemma OAI.HardSphere.Groups.datumPermitted_measurable line 144