OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumOrderedSpatial.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Exact cell maps for the five literal early stages. No vertex or term enumeration is changed while assigning the mediator cells.

  1. def OAI.ContinuumCoulomb.QuantumOrderedSpatial.anchor1 line 16
  2. def OAI.ContinuumCoulomb.QuantumOrderedSpatial.anchor2 line 17
  3. def OAI.ContinuumCoulomb.QuantumOrderedSpatial.anchor3 line 18
  4. def OAI.ContinuumCoulomb.QuantumOrderedSpatial.anchor4 line 19
  5. def OAI.ContinuumCoulomb.QuantumOrderedSpatial.outputAnchor line 20
  6. def OAI.ContinuumCoulomb.QuantumOrderedSpatial.cell1 line 22
  7. def OAI.ContinuumCoulomb.QuantumOrderedSpatial.cell2 line 24
  8. def OAI.ContinuumCoulomb.QuantumOrderedSpatial.cell3 line 26
  9. def OAI.ContinuumCoulomb.QuantumOrderedSpatial.cell4 line 28
  10. def OAI.ContinuumCoulomb.QuantumOrderedSpatial.outputCell line 30
  11. theorem OAI.ContinuumCoulomb.QuantumOrderedSpatial.output_near line 35
  12. theorem OAI.ContinuumCoulomb.QuantumOrderedSpatial.anchor1_card line 52
  13. theorem OAI.ContinuumCoulomb.QuantumOrderedSpatial.anchor2_card line 59
  14. theorem OAI.ContinuumCoulomb.QuantumOrderedSpatial.anchor3_card line 69
  15. theorem OAI.ContinuumCoulomb.QuantumOrderedSpatial.anchor4_card line 79
  16. theorem OAI.ContinuumCoulomb.QuantumOrderedSpatial.outputAnchor_card line 89
  17. theorem OAI.ContinuumCoulomb.QuantumOrderedSpatial.outputCell_card line 99
  18. theorem OAI.ContinuumCoulomb.QuantumOrderedSpatial.output_density line 127