OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumDescriptorSites.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The descriptor compiler computes the very same ordered support labels as the mathematical local-history construction.

  1. def OAI.ContinuumCoulomb.QuantumHistoryDescriptors.distributedLabels line 14
  2. theorem OAI.ContinuumCoulomb.QuantumHistoryDescriptors.distributedLabels_actual line 23
  3. def OAI.ContinuumCoulomb.QuantumHistoryDescriptors.referenceWork line 41
  4. theorem OAI.ContinuumCoulomb.QuantumHistoryDescriptors.referenceWork_eq line 43
  5. def OAI.ContinuumCoulomb.QuantumHistoryDescriptors.orderedAt line 45
  6. theorem OAI.ContinuumCoulomb.QuantumHistoryDescriptors.orderedAt_actual line 48
  7. def OAI.ContinuumCoulomb.QuantumHistoryDescriptors.rebitLabels line 56
  8. def OAI.ContinuumCoulomb.QuantumHistoryDescriptors.referenceLabels line 59
  9. theorem OAI.ContinuumCoulomb.QuantumHistoryDescriptors.number_inr line 63
  10. theorem OAI.ContinuumCoulomb.QuantumHistoryDescriptors.rebitLabels_actual line 69
  11. theorem OAI.ContinuumCoulomb.QuantumHistoryDescriptors.referenceLabels_actual line 82
  12. def OAI.ContinuumCoulomb.QuantumHistoryDescriptors.supportLabels line 98
  13. theorem OAI.ContinuumCoulomb.QuantumHistoryDescriptors.supportLabels_actual line 100