OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumOrderedSpatialSites.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The literal early compiler places each mediator at the anchor of its source word. These geometric statements retain the exact ordered word types.

  1. def OAI.ContinuumCoulomb.QuantumOrderedSpatial.Near line 16
  2. theorem OAI.ContinuumCoulomb.QuantumOrderedSpatial.map_near line 20
  3. theorem OAI.ContinuumCoulomb.QuantumOrderedSpatial.append_near line 29
  4. theorem OAI.ContinuumCoulomb.QuantumOrderedSpatial.subdivision_near line 41
  5. theorem OAI.ContinuumCoulomb.QuantumOrderedSpatial.third_near line 61
  6. theorem OAI.ContinuumCoulomb.QuantumOrderedSpatial.yy_near line 95