OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumOrderedLabelSubdivision.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Literal bounded arrays for polarized subdivision. The exact array identity below keeps the supplied site order and the matching mediator.

  1. def OAI.ContinuumCoulomb.QuantumOrderedLabelData.subdivision line 14
  2. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelData.tag_lift line 19
  3. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelData.tag_appendMediator line 25
  4. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelData.first_tag line 34
  5. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelData.second_tag line 41
  6. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelData.first_axis line 48
  7. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelData.subdivision_tag line 60