OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumOrdinalSlots.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Explicit ordinal ranks give the required injective slots in each bounded cell fiber. This is the finite ordering used by the spatial output program.

  1. def OAI.ContinuumCoulomb.QuantumOrdinalSlots.before line 10
  2. def OAI.ContinuumCoulomb.QuantumOrdinalSlots.rank line 13
  3. theorem OAI.ContinuumCoulomb.QuantumOrdinalSlots.rank_lt_fiber line 15
  4. theorem OAI.ContinuumCoulomb.QuantumOrdinalSlots.rank_lt line 25
  5. theorem OAI.ContinuumCoulomb.QuantumOrdinalSlots.rank_injective_on_cell line 37
  6. def OAI.ContinuumCoulomb.QuantumOrdinalSlots.slot line 46
  7. theorem OAI.ContinuumCoulomb.QuantumOrdinalSlots.slot_injective_on_cell line 50