OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumSupportDedup.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The support compiler retains the last occurrence of each numeric label, exactly as List.dedup does in the mathematical ordered support.

  1. def OAI.ContinuumCoulomb.QuantumSupportDedup.insert line 14
  2. theorem OAI.ContinuumCoulomb.QuantumSupportDedup.insert_sublist line 16
  3. theorem OAI.ContinuumCoulomb.QuantumSupportDedup.fold_sublist line 22
  4. theorem OAI.ContinuumCoulomb.QuantumSupportDedup.fold_bound line 30
  5. theorem OAI.ContinuumCoulomb.QuantumSupportDedup.foldr_eq line 38
  6. opaque OAI.ContinuumCoulomb.QuantumSupportDedup.insertProgram line 45
  7. opaque OAI.ContinuumCoulomb.QuantumSupportDedup.foldProgram line 52
  8. opaque OAI.ContinuumCoulomb.QuantumSupportDedup.program line 62