OAI/Analysis/HardSphere/Bridges/PhysicalSparse.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.Bridge.physicalEdges line 19
  2. instance OAI.HardSphere.Bridge.physicalEdges_fintype line 22
  3. def OAI.HardSphere.Bridge.physicalSparseChecks line 25
  4. lemma OAI.HardSphere.Bridge.physicalSparseChecks_complete line 31
  5. lemma OAI.HardSphere.Bridge.physicalSparseChecks_degree line 48
  6. lemma OAI.HardSphere.Bridge.physicalSparseChecks_insertion line 75
  7. def OAI.HardSphere.Bridge.fiberEquiv line 114
  8. lemma OAI.HardSphere.Bridge.fiberEquiv_pi line 118
  9. lemma OAI.HardSphere.Bridge.fiberEquiv_self line 122
  10. lemma OAI.HardSphere.Bridge.move_mem_iff line 127
  11. def OAI.HardSphere.Bridge.routeOwner line 138
  12. lemma OAI.HardSphere.Bridge.routeOwner_injective line 140
  13. def OAI.HardSphere.Bridge.routePath line 146
  14. lemma OAI.HardSphere.Bridge.routePath_measurable line 156
  15. def OAI.HardSphere.Bridge.routeChecks line 167
  16. def OAI.HardSphere.Bridge.primaryChecks line 172
  17. lemma OAI.HardSphere.Bridge.routeChecks_primary line 177
  18. lemma OAI.HardSphere.Bridge.routePath_unselected line 186
  19. lemma OAI.HardSphere.Bridge.routeChecks_outside line 195