OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumLaneSupport.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Lane expansion preserves disjoint paths; different lanes meet only transversely.

  1. def OAI.ContinuumCoulomb.qmaLaneDown line 10
  2. theorem OAI.ContinuumCoulomb.qmaLaneDown_point line 12
  3. def OAI.ContinuumCoulomb.qmaLaneSupport line 18
  4. theorem OAI.ContinuumCoulomb.qmaLaneSupport_down line 21
  5. theorem OAI.ContinuumCoulomb.qmaLaneSupport_disjoint line 49
  6. theorem OAI.ContinuumCoulomb.qmaLaneSupport_transverse line 56
  7. theorem OAI.ContinuumCoulomb.qmaLaneSupport_two_crossings line 66
  8. theorem OAI.ContinuumCoulomb.qmaLaneSupport_crossing_not_vertex line 73