OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumForkPorts.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Private active ports remain private after a simultaneous fork round.

  1. abbrev OAI.ContinuumCoulomb.QMAForkPair line 13
  2. abbrev OAI.ContinuumCoulomb.QMAForkRemainder line 14
  3. def OAI.ContinuumCoulomb.qmaForkAllPortEquiv line 16
  4. def OAI.ContinuumCoulomb.qmaForkPairedPort line 22
  5. def OAI.ContinuumCoulomb.qmaForkRemainingPort line 26
  6. theorem OAI.ContinuumCoulomb.qmaForkPairedPort_injective line 29
  7. theorem OAI.ContinuumCoulomb.qmaForkRemainingPort_injective line 34
  8. theorem OAI.ContinuumCoulomb.qmaForkPairedPort_ne_remaining line 38
  9. structure OAI.ContinuumCoulomb.QMAForkPorts line 45
  10. abbrev OAI.ContinuumCoulomb.QMAForkPorts.pairCount line 55
  11. def OAI.ContinuumCoulomb.QMAForkPorts.pairEquiv line 56
  12. def OAI.ContinuumCoulomb.QMAForkPorts.site line 58
  13. theorem OAI.ContinuumCoulomb.QMAForkPorts.site_injective line 63
  14. theorem OAI.ContinuumCoulomb.QMAForkPorts.outer_injective line 77
  15. def OAI.ContinuumCoulomb.QMAForkPorts.nextPortEquiv line 87
  16. def OAI.ContinuumCoulomb.QMAForkPorts.nextPortAux line 92
  17. theorem OAI.ContinuumCoulomb.QMAForkPorts.nextPortAux_injective line 96
  18. def OAI.ContinuumCoulomb.QMAForkPorts.next line 108
  19. theorem OAI.ContinuumCoulomb.QMAForkPorts.pairCount_bound line 121