OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumRetainedCrossing.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Every edge internal to a selected crossing is removed from the retained graph. The assertion concerns the actual completed subdivision graph.

  1. theorem OAI.ContinuumCoulomb.qmaCrossPair_direction line 14
  2. theorem OAI.ContinuumCoulomb.QMAPortRouteData.finished_edge_adjacent line 31
  3. theorem OAI.ContinuumCoulomb.QMAPortRouteData.graph_link line 37
  4. theorem OAI.ContinuumCoulomb.QMAPortRouteData.finished_edge_link line 45
  5. theorem OAI.ContinuumCoulomb.QMAPortRouteData.retained_no_internal_crossing line 51