OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumCellTranslate.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Cell-local paths translate injectively and different cells are disjoint.

  1. def OAI.ContinuumCoulomb.qmaCellTranslate line 9
  2. theorem OAI.ContinuumCoulomb.qmaCellTranslate_injective line 11
  3. theorem OAI.ContinuumCoulomb.qmaCellTranslate_cell line 16
  4. theorem OAI.ContinuumCoulomb.qmaCellTranslate_unique line 20
  5. theorem OAI.ContinuumCoulomb.qmaCellTranslate_step line 28
  6. theorem OAI.ContinuumCoulomb.qmaCellTranslate_port line 34
  7. theorem OAI.ContinuumCoulomb.qmaCellTranslate_inner line 38
  8. theorem OAI.ContinuumCoulomb.qmaCellTranslate_patch line 42