OAI/Analysis/HardSphere/Allocation/PhysicalVertex.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.Bridge.exposedPeriodPair_at line 16
  2. lemma OAI.HardSphere.Groups.datumAccessible_endpoints line 84
  3. lemma OAI.HardSphere.Groups.midpoint_bound line 99
  4. lemma OAI.HardSphere.Groups.unitTarget_sub line 113
  5. def OAI.HardSphere.Groups.routeCellPeriod line 117
  6. lemma OAI.HardSphere.Groups.routeCellPeriod_chart line 120
  7. def OAI.HardSphere.Groups.vertexTarget line 125
  8. lemma OAI.HardSphere.Groups.vertexTarget_measurable line 133
  9. lemma OAI.HardSphere.Groups.vertexTarget_subset line 142
  10. lemma OAI.HardSphere.Groups.vertexTarget_volume line 148
  11. def OAI.HardSphere.Groups.shiftedDatumPermitted line 191
  12. lemma OAI.HardSphere.Groups.shiftedDatumPermitted_measurable line 196
  13. lemma OAI.HardSphere.Groups.shiftedDatumPermitted_equiv line 202
  14. lemma OAI.HardSphere.Groups.datumSuccess_shift line 209
  15. def OAI.HardSphere.Groups.vertexPair line 223
  16. instance OAI.HardSphere.Groups.vertexPair_finite line 240
  17. def OAI.HardSphere.Groups.vertexDensityBound line 247
  18. theorem OAI.HardSphere.Groups.vertexPair_physical line 250