OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPlanarSelectorTransport.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The actual finite selector gives a planar family after arbitrary vertex and edge permutations, including independent edge orientation changes.

  1. theorem OAI.ContinuumCoulomb.QMAPlanarListData.range_toRoute_point line 15
  2. theorem OAI.ContinuumCoulomb.QMAPortRouteData.crossing_hasAllowedRoute line 34
  3. def OAI.ContinuumCoulomb.QMAPortRouteData.selectorTransportRoute line 59
  4. theorem OAI.ContinuumCoulomb.QMAPortRouteData.selectorTransportRoute_spec line 64
  5. theorem OAI.ContinuumCoulomb.QMAPortRouteData.selectorTransportRoute_path line 73
  6. theorem OAI.ContinuumCoulomb.QMAPortRouteData.selectorTransportRoute_endpointPair line 80
  7. theorem OAI.ContinuumCoulomb.QMAPortRouteData.selectorTransportRoute_pairs_injective line 91
  8. def OAI.ContinuumCoulomb.QMAPortRouteData.selectorPlanarList line 101
  9. theorem OAI.ContinuumCoulomb.QMAPortRouteData.selectorPlanarList_path line 134
  10. def OAI.ContinuumCoulomb.QMAPortRouteData.selectorPlanarRoute line 142
  11. theorem OAI.ContinuumCoulomb.QMAPortRouteData.selectorPlanarRoute_path line 147
  12. theorem OAI.ContinuumCoulomb.QMAPortRouteData.selectorPlanarRoute_length line 157
  13. theorem OAI.ContinuumCoulomb.QMAPortRouteData.selectorTransportRoute_path_bounded line 164
  14. theorem OAI.ContinuumCoulomb.QMAPortRouteData.selectorPlanarRoute_bounded line 177