OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumCrossingSites.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Every terminal of every selected crossing is an actual spin in the completed rational port graph. Distinct crossing cells have disjoint terminal sets.

  1. abbrev OAI.ContinuumCoulomb.QMAPortRouteData.Crossing line 15
  2. abbrev OAI.ContinuumCoulomb.QMAPortRouteData.finishedGraph line 17
  3. def OAI.ContinuumCoulomb.QMAPortRouteData.finishedPosition line 19
  4. theorem OAI.ContinuumCoulomb.QMAPortRouteData.crossing_terminal_exists line 22
  5. def OAI.ContinuumCoulomb.QMAPortRouteData.crossingSite line 38
  6. theorem OAI.ContinuumCoulomb.QMAPortRouteData.crossingSite_spec line 41
  7. theorem OAI.ContinuumCoulomb.QMAPortRouteData.crossingSite_injective line 45