OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumCellCrossings.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

An exact finite set of crossing cells, selected from the route visits.

  1. def OAI.ContinuumCoulomb.QMAPortRouteData.pairing line 13
  2. theorem OAI.ContinuumCoulomb.QMAPortRouteData.pairing_classify line 16
  3. def OAI.ContinuumCoulomb.QMAPortRouteData.IsCrossing line 21
  4. def OAI.ContinuumCoulomb.QMAPortRouteData.crossingCells line 24
  5. theorem OAI.ContinuumCoulomb.QMAPortRouteData.mem_crossingCells line 26
  6. theorem OAI.ContinuumCoulomb.QMAPortRouteData.crossingCells_card line 34