OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumEvenRouteLabels.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Explicit vertex and edge labels for the even subdivision of a planar route family.

  1. def OAI.ContinuumCoulomb.QuantumEvenRouteLabels.selectedEquiv line 16
  2. def OAI.ContinuumCoulomb.QuantumEvenRouteLabels.activeIndex line 29
  3. theorem OAI.ContinuumCoulomb.QuantumEvenRouteLabels.selected_index line 32
  4. def OAI.ContinuumCoulomb.QuantumEvenRouteLabels.vertex line 36
  5. theorem OAI.ContinuumCoulomb.QuantumEvenRouteLabels.vertex_old line 41
  6. theorem OAI.ContinuumCoulomb.QuantumEvenRouteLabels.vertex_fresh line 45
  7. def OAI.ContinuumCoulomb.QuantumEvenRouteLabels.edge line 51
  8. def OAI.ContinuumCoulomb.QuantumEvenRouteLabels.unedge line 55
  9. def OAI.ContinuumCoulomb.QuantumEvenRouteLabels.edgeEquiv line 60
  10. def OAI.ContinuumCoulomb.QuantumEvenRouteLabels.work line 81
  11. theorem OAI.ContinuumCoulomb.QuantumEvenRouteLabels.work_eq line 83
  12. def OAI.ContinuumCoulomb.QuantumEvenRouteLabels.originalPath line 93
  13. theorem OAI.ContinuumCoulomb.QuantumEvenRouteLabels.fresh_eq line 96
  14. theorem OAI.ContinuumCoulomb.QuantumEvenRouteLabels.paths_eq line 103
  15. theorem OAI.ContinuumCoulomb.QuantumEvenRouteLabels.positions_eq line 140
  16. theorem OAI.ContinuumCoulomb.QuantumEvenRouteLabels.allPaths_eq line 167