OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumChosenSlots.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Geometry only needs a bounded slot map injective inside each cell. This interface permits the literal ordinal slot map without fixing abstract choices.

  1. structure OAI.ContinuumCoulomb.QMACellSlots line 11
  2. def OAI.ContinuumCoulomb.QMACellSlots.ofDensity line 19
  3. def OAI.ContinuumCoulomb.QMACellSlots.site line 23
  4. theorem OAI.ContinuumCoulomb.QMACellSlots.site_injective line 26
  5. theorem OAI.ContinuumCoulomb.QMACellSlots.site_cell line 37
  6. theorem OAI.ContinuumCoulomb.QMACellSlots.site_bounds line 45
  7. theorem OAI.ContinuumCoulomb.QMACellSlots.route_length line 57
  8. def OAI.ContinuumCoulomb.QMACellSlots.color line 67
  9. theorem OAI.ContinuumCoulomb.QMACellSlots.color_eq line 71
  10. theorem OAI.ContinuumCoulomb.QMACellSlots.color_disjoint line 82