OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPlanarRelabel.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Transport a planar route family through vertex and edge permutations. Each edge may independently reverse its orientation.

  1. def OAI.ContinuumCoulomb.QMAPlanarRouteData.relabelIndex line 12
  2. theorem OAI.ContinuumCoulomb.QMAPlanarRouteData.relabelIndex_le line 15
  3. theorem OAI.ContinuumCoulomb.QMAPlanarRouteData.relabelIndex_interior line 21
  4. theorem OAI.ContinuumCoulomb.QMAPlanarRouteData.relabelIndex_injective line 26
  5. def OAI.ContinuumCoulomb.QMAPlanarRouteData.relabelStepIndex line 31
  6. theorem OAI.ContinuumCoulomb.QMAPlanarRouteData.relabelStepIndex_lt line 34
  7. theorem OAI.ContinuumCoulomb.QMAPlanarRouteData.relabelIndex_left line 38
  8. theorem OAI.ContinuumCoulomb.QMAPlanarRouteData.relabelIndex_right line 46
  9. theorem OAI.ContinuumCoulomb.QMAPlanarRouteData.flip_pairs_disjoint line 51
  10. def OAI.ContinuumCoulomb.QMAPlanarRouteData.relabel line 64
  11. theorem OAI.ContinuumCoulomb.QMAPlanarRouteData.relabel_position line 113
  12. theorem OAI.ContinuumCoulomb.QMAPlanarRouteData.relabel_point line 116
  13. theorem OAI.ContinuumCoulomb.QMAPlanarRouteData.relabel_length_le line 120
  14. theorem OAI.ContinuumCoulomb.QMAPlanarRouteData.relabel_bounded line 123