OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/FiniteOrbitalComplement.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The complement occupation bound for a finite family requires no choice of ambient basis in its statement. The auxiliary basis is constructed.

  1. theorem OAI.ContinuumCoulomb.finite_orbital_complement_bound line 14