OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumOrderedSpatialComplete.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Spatial data for the literal ordered six-stage compiler. A mediator is placed in its parent term's cell, and each emitted term retains that anchor.

  1. def OAI.ContinuumCoulomb.QuantumOrderedSpatialComplete.extendCell line 14
  2. def OAI.ContinuumCoulomb.QuantumOrderedSpatialComplete.extendAnchor line 15
  3. theorem OAI.ContinuumCoulomb.QuantumOrderedSpatialComplete.extension_geometry line 17
  4. theorem OAI.ContinuumCoulomb.QuantumOrderedSpatialComplete.extendCell_density line 32
  5. theorem OAI.ContinuumCoulomb.QuantumOrderedSpatialComplete.extendAnchor_density line 39
  6. def OAI.ContinuumCoulomb.QuantumOrderedSpatialComplete.cell1 line 46
  7. def OAI.ContinuumCoulomb.QuantumOrderedSpatialComplete.anchor1 line 47
  8. def OAI.ContinuumCoulomb.QuantumOrderedSpatialComplete.cell2 line 48
  9. def OAI.ContinuumCoulomb.QuantumOrderedSpatialComplete.anchor2 line 49
  10. def OAI.ContinuumCoulomb.QuantumOrderedSpatialComplete.cell3 line 50
  11. def OAI.ContinuumCoulomb.QuantumOrderedSpatialComplete.anchor3 line 51
  12. def OAI.ContinuumCoulomb.QuantumOrderedSpatialComplete.cell4 line 52
  13. def OAI.ContinuumCoulomb.QuantumOrderedSpatialComplete.anchor4 line 53
  14. def OAI.ContinuumCoulomb.QuantumOrderedSpatialComplete.cell5 line 54
  15. def OAI.ContinuumCoulomb.QuantumOrderedSpatialComplete.anchor5 line 55
  16. def OAI.ContinuumCoulomb.QuantumOrderedSpatialComplete.cell6 line 56
  17. def OAI.ContinuumCoulomb.QuantumOrderedSpatialComplete.anchor6 line 57
  18. theorem OAI.ContinuumCoulomb.QuantumOrderedSpatialComplete.complete_geometry line 61
  19. theorem OAI.ContinuumCoulomb.QuantumOrderedSpatialComplete.complete_density line 88