OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumCellPassages.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

A visit to an internal coarse cell occupies two different directional ports.

  1. abbrev OAI.ContinuumCoulomb.QMAPortRouteData.Interior line 12
  2. def OAI.ContinuumCoulomb.QMAPortRouteData.cell line 14
  3. def OAI.ContinuumCoulomb.QMAPortRouteData.armIndex line 16
  4. def OAI.ContinuumCoulomb.QMAPortRouteData.arm line 18
  5. theorem OAI.ContinuumCoulomb.QMAPortRouteData.cell_index_lt line 20
  6. theorem OAI.ContinuumCoulomb.QMAPortRouteData.armIndex_le line 24
  7. theorem OAI.ContinuumCoulomb.QMAPortRouteData.arm_adjacent line 30
  8. def OAI.ContinuumCoulomb.QMAPortRouteData.port line 36
  9. theorem OAI.ContinuumCoulomb.QMAPortRouteData.port_spec line 38
  10. theorem OAI.ContinuumCoulomb.QMAPortRouteData.port_injective line 43
  11. theorem OAI.ContinuumCoulomb.QMAPortRouteData.cell_eq_same_edge line 53
  12. theorem OAI.ContinuumCoulomb.QMAPortRouteData.incidence_injective line 64