OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumUnaryEmbedding.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Isometric embedding of the finite history into all unary clock strings.

  1. def OAI.ContinuumCoulomb.qmaUnaryInclusion line 12
  2. theorem OAI.ContinuumCoulomb.qmaUnaryInclusion_injective line 15
  3. def OAI.ContinuumCoulomb.qmaUnaryExtend line 23
  4. theorem OAI.ContinuumCoulomb.qmaUnaryExtend_valid line 26
  5. theorem OAI.ContinuumCoulomb.qmaUnaryExtend_zero line 31
  6. theorem OAI.ContinuumCoulomb.qmaUnaryRestrict_extend line 40
  7. theorem OAI.ContinuumCoulomb.qmaUnaryExtend_invalid_mass line 45
  8. theorem OAI.ContinuumCoulomb.qmaUnaryExtend_mass line 53
  9. theorem OAI.ContinuumCoulomb.qmaUnaryExtend_clock_energy line 57
  10. theorem OAI.ContinuumCoulomb.qmaUnaryResidual_extend_invalid line 65