OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumEndpointRelabel.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The unordered endpoint support determines the edge permutation of a simple graph, including the possible reversal of each edge.

  1. def OAI.ContinuumCoulomb.QuantumEndpointRelabel.chooseEdge line 19
  2. theorem OAI.ContinuumCoulomb.QuantumEndpointRelabel.chooseEdge_spec line 21
  3. theorem OAI.ContinuumCoulomb.QuantumEndpointRelabel.chooseEdge_injective line 27
  4. theorem OAI.ContinuumCoulomb.QuantumEndpointRelabel.endpoint_injective line 38
  5. theorem OAI.ContinuumCoulomb.QuantumEndpointRelabel.chooseEdge_surjective line 46
  6. def OAI.ContinuumCoulomb.QuantumEndpointRelabel.edge line 52
  7. def OAI.ContinuumCoulomb.QuantumEndpointRelabel.flip line 55
  8. theorem OAI.ContinuumCoulomb.QuantumEndpointRelabel.left line 57
  9. theorem OAI.ContinuumCoulomb.QuantumEndpointRelabel.right line 72