OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumScheduleCrossingGeometry.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Match the complete literal crossing packet to the canonical port crossing geometry. The input schedule and the crossing cells may have arbitrary orders.

  1. def OAI.ContinuumCoulomb.QuantumScheduleCrossingGeometry.site line 27
  2. theorem OAI.ContinuumCoulomb.QuantumScheduleCrossingGeometry.site_global line 30
  3. theorem OAI.ContinuumCoulomb.QuantumScheduleCrossingGeometry.site_injective line 33
  4. def OAI.ContinuumCoulomb.QuantumScheduleCrossingGeometry.layer line 37
  5. def OAI.ContinuumCoulomb.QuantumScheduleCrossingGeometry.input line 41
  6. theorem OAI.ContinuumCoulomb.QuantumScheduleCrossingGeometry.input_actual line 45
  7. def OAI.ContinuumCoulomb.QuantumScheduleCrossingGeometry.vertex line 54
  8. theorem OAI.ContinuumCoulomb.QuantumScheduleCrossingGeometry.layer_support line 59
  9. theorem OAI.ContinuumCoulomb.QuantumScheduleCrossingGeometry.output_support line 79
  10. theorem OAI.ContinuumCoulomb.QuantumScheduleCrossingGeometry.positions_actual line 103
  11. theorem OAI.ContinuumCoulomb.QuantumScheduleCrossingGeometry.packet_geometry line 114