OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumScaledDirection.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Interior points of two scaled unit segments can coincide only when the underlying grid edge is the same, possibly with reversed orientation.

  1. def OAI.ContinuumCoulomb.qmaScaledDirectionPoint line 10
  2. theorem OAI.ContinuumCoulomb.qmaScaledDirectionPoint_eq line 14
  3. theorem OAI.ContinuumCoulomb.qmaScaledDirectionPoint_not_center line 24
  4. theorem OAI.ContinuumCoulomb.qmaScaledDirectionPoint_collision line 32
  5. theorem OAI.ContinuumCoulomb.qmaScaledEdge_inner_collision line 45