OAI/Analysis/HardSphere/Allocation/RouteFields.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.Groups.RouteFieldValid line 19
  2. def OAI.HardSphere.Groups.fieldLabels line 21
  3. lemma OAI.HardSphere.Groups.fieldLabels_spec line 23
  4. lemma OAI.HardSphere.Groups.branchAccessible_home line 27
  5. lemma OAI.HardSphere.Groups.routeFieldValid_of_supported line 34
  6. lemma OAI.HardSphere.Groups.fieldLabels_physical line 55
  7. lemma OAI.HardSphere.Groups.simpleRouteLength_eq line 70
  8. def OAI.HardSphere.Groups.fieldRouteLabels line 74
  9. lemma OAI.HardSphere.Groups.fieldRouteLabels_physical line 78
  10. abbrev OAI.HardSphere.Groups.PhysicalRouteCode line 105
  11. def OAI.HardSphere.Groups.physicalCodedRoute line 108
  12. lemma OAI.HardSphere.Groups.physicalCodedRoute_mass_le_one line 118
  13. instance OAI.HardSphere.Groups.physicalCodedRoute_finite line 127
  14. def OAI.HardSphere.Groups.physicalRouteFamily line 133
  15. instance OAI.HardSphere.Groups.physicalRouteFamily_finite line 141
  16. def OAI.HardSphere.Groups.physicalMixedRoutes line 146
  17. instance OAI.HardSphere.Groups.physicalMixedRoutes_finite line 153
  18. lemma OAI.HardSphere.Groups.physicalMixedRoutes_mass_le_one line 159