OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPathCoverage.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Every prescribed path point becomes an actual spin when subdivision finishes.

  1. theorem OAI.ContinuumCoulomb.QMAPathEmbedding.next_covers_point line 14
  2. def OAI.ContinuumCoulomb.QMAPathEmbedding.Occupied line 46
  3. theorem OAI.ContinuumCoulomb.QMAPathEmbedding.next_occupied line 49
  4. theorem OAI.ContinuumCoulomb.QMAPathEmbedding.iterate_occupied line 55
  5. theorem OAI.ContinuumCoulomb.QMAPathEmbedding.occupied_complete line 61
  6. theorem OAI.ContinuumCoulomb.QMAPathEmbedding.iterate_covers_point line 75