OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumCorridorInterior.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

An interior corridor point belongs to the nonterminal part of one of its two cell-local halves.

  1. theorem OAI.ContinuumCoulomb.qmaListInterior_ne_head line 10
  2. theorem OAI.ContinuumCoulomb.qmaListInterior_ne_last line 18
  3. theorem OAI.ContinuumCoulomb.qmaList_mem_drop_one line 26
  4. theorem OAI.ContinuumCoulomb.qmaCellCorridor_interior line 33