OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPlanarRouteData.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A planar route family supplies the even physical subdivision data explicitly, including its four-direction reserved leaf sites.

  1. structure OAI.ContinuumCoulomb.QMAPlanarRouteData line 13
  2. def OAI.ContinuumCoulomb.QMAPlanarRouteData.direction line 33
  3. theorem OAI.ContinuumCoulomb.QMAPlanarRouteData.direction_spec line 35
  4. def OAI.ContinuumCoulomb.QMAPlanarRouteData.leaf line 40
  5. theorem OAI.ContinuumCoulomb.QMAPlanarRouteData.leaf_injective line 42
  6. theorem OAI.ContinuumCoulomb.QMAPlanarRouteData.even_length line 52
  7. def OAI.ContinuumCoulomb.QMAPlanarRouteData.toEven line 56