OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPermittedEndpointAvoidance.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

An interior point of a permitted path cannot be an endpoint of any other permitted path, including catalog paths not present in the Hamiltonian.

  1. theorem OAI.ContinuumCoulomb.QMAPortRouteData.permitted_avoids_source line 14