OAI/Analysis/HardSphere/Allocation/PhysicalPrimary.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.Comparison.conditioned_prod_univ line 15
  2. lemma OAI.HardSphere.Comparison.conditioned_option line 22
  3. def OAI.HardSphere.Groups.physicalSlotMutual line 41
  4. lemma OAI.HardSphere.Groups.physicalSlotMutual_measurable line 44
  5. def OAI.HardSphere.Groups.physicalPrimaryReference line 49
  6. instance OAI.HardSphere.Groups.physicalPrimaryReference_finite line 56
  7. lemma OAI.HardSphere.Groups.physicalPrimaryReference_apply line 63
  8. theorem OAI.HardSphere.Groups.physicalPrimaryReference_actual line 75
  9. def OAI.HardSphere.Groups.physicalSharedRoute line 88
  10. instance OAI.HardSphere.Groups.physicalSharedRoute_finite line 99
  11. def OAI.HardSphere.Groups.physicalSlotAllowed line 119
  12. lemma OAI.HardSphere.Groups.physicalSlotAllowed_measurable line 126
  13. def OAI.HardSphere.Groups.physicalSlotOn line 134
  14. lemma OAI.HardSphere.Groups.physicalSlotOn_map line 143
  15. instance OAI.HardSphere.Groups.physicalSlotOn_finite line 161
  16. lemma OAI.HardSphere.Groups.physicalSlotOn_probability line 171
  17. lemma OAI.HardSphere.Groups.physicalAllowed_confined line 181
  18. lemma OAI.HardSphere.Groups.physicalAllowed_checks line 188
  19. lemma OAI.HardSphere.Groups.physicalPrimary_on_map line 210