OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumTranslatedPatch.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Translating the fixed crossing patch to every isolated route crossing.

  1. def OAI.ContinuumCoulomb.qmaPatchTranslate line 10
  2. theorem OAI.ContinuumCoulomb.qmaPatchTranslate_injective line 12
  3. theorem OAI.ContinuumCoulomb.qmaPatchTranslate_distance line 18
  4. theorem OAI.ContinuumCoulomb.qmaPatchTranslate_mem line 24
  5. theorem OAI.ContinuumCoulomb.qmaPatchTranslate_ne line 30
  6. def OAI.ContinuumCoulomb.qmaCrossingPathAt line 39
  7. theorem OAI.ContinuumCoulomb.qmaCrossingPathAt_chain line 42
  8. theorem OAI.ContinuumCoulomb.qmaCrossingPathAt_simple line 49
  9. theorem OAI.ContinuumCoulomb.qmaCrossingPathAt_mem line 52
  10. theorem OAI.ContinuumCoulomb.qmaCrossingPathAt_disjoint line 57
  11. def OAI.ContinuumCoulomb.qmaCrossingPortAt line 65
  12. theorem OAI.ContinuumCoulomb.qmaCrossingPortAt_step line 69
  13. theorem OAI.ContinuumCoulomb.qmaCrossingPortAt_outside line 76