OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPlanarDegree.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Disjoint lattice routes bound the actual edge-incidence degree by the four available lattice directions, including edges whose orientation points inward.

  1. abbrev OAI.ContinuumCoulomb.QMAPlanarRouteData.Incident line 15
  2. def OAI.ContinuumCoulomb.QMAPlanarRouteData.incidentNear line 17
  3. theorem OAI.ContinuumCoulomb.QMAPlanarRouteData.incident_segment line 20
  4. theorem OAI.ContinuumCoulomb.QMAPlanarRouteData.incident_position_positive line 35
  5. theorem OAI.ContinuumCoulomb.QMAPlanarRouteData.incident_adjacent line 41
  6. theorem OAI.ContinuumCoulomb.QMAPlanarRouteData.incidentNear_injective line 49
  7. def OAI.ContinuumCoulomb.QMAPlanarRouteData.incidentDirection line 62
  8. theorem OAI.ContinuumCoulomb.QMAPlanarRouteData.incidentDirection_injective line 65
  9. theorem OAI.ContinuumCoulomb.QMAPlanarRouteData.degree_le_four line 74