OAI/Analysis/HardSphere/Conditioning/PhysicalRoute.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.Comparison.routePosition line 15
  2. lemma OAI.HardSphere.Comparison.routeEmbedding_position line 18
  3. def OAI.HardSphere.Comparison.routeSlotEquiv line 22
  4. lemma OAI.HardSphere.Comparison.routePermutation_symm_first line 28
  5. lemma OAI.HardSphere.Comparison.routePermutation_symm_later line 34
  6. def OAI.HardSphere.Groups.physicalSlotReference line 48
  7. instance OAI.HardSphere.Groups.physicalSlotReference_finite line 55
  8. lemma OAI.HardSphere.Groups.physicalSlot_first line 61
  9. lemma OAI.HardSphere.Groups.physicalSlot_second line 76
  10. def OAI.HardSphere.Groups.physicalSelectedFactor line 91
  11. instance OAI.HardSphere.Groups.physicalSelectedFactor_finite line 98
  12. theorem OAI.HardSphere.Groups.physicalSelectedFactor_physical line 105