OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumRetainedSupport.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Filtering the bond tape retains exactly the unselected physical edges, including their orientation, regardless of their list order.

  1. theorem OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.retained_edge_source line 18
  2. theorem OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.retained_edge_target line 38