OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPatchSeparation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Disjoint twelve-wide crossing patches after a fixed integer expansion.

  1. def OAI.ContinuumCoulomb.qmaExpandedPoint line 9
  2. def OAI.ContinuumCoulomb.qmaPatchBox line 10
  3. theorem OAI.ContinuumCoulomb.qmaExpandedPoint_dist_row line 13
  4. theorem OAI.ContinuumCoulomb.qmaExpandedPoint_dist_col line 17
  5. theorem OAI.ContinuumCoulomb.qmaPatchBox_disjoint line 21
  6. theorem OAI.ContinuumCoulomb.qmaExpandedPoint_mem_own line 35
  7. theorem OAI.ContinuumCoulomb.qmaExpandedPoint_not_mem line 38
  8. theorem OAI.ContinuumCoulomb.qmaExpandedCrossing_not_vertex line 43