OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPlanarTapeSupport.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The actual merged planar tape and the canonical crossing graph have the same unordered edges, with an explicit finite edge equivalence.

  1. def OAI.ContinuumCoulomb.QuantumPlanarTapeGeometry.rawGraph line 15
  2. def OAI.ContinuumCoulomb.QuantumPlanarTapeGeometry.graph line 19
  3. theorem OAI.ContinuumCoulomb.QuantumPlanarTapeGeometry.fin_pair_eq line 23
  4. theorem OAI.ContinuumCoulomb.QuantumPlanarTapeGeometry.graph_source line 29
  5. theorem OAI.ContinuumCoulomb.QuantumPlanarTapeGeometry.graph_target line 42
  6. theorem OAI.ContinuumCoulomb.QuantumPlanarTapeGeometry.graph_simple line 55
  7. theorem OAI.ContinuumCoulomb.QuantumPlanarTapeGeometry.canonical_source line 79
  8. theorem OAI.ContinuumCoulomb.QuantumPlanarTapeGeometry.canonical_target line 89
  9. def OAI.ContinuumCoulomb.QuantumPlanarTapeGeometry.edge line 98
  10. theorem OAI.ContinuumCoulomb.QuantumPlanarTapeGeometry.edge_endpoints line 103