OAI/Analysis/KadisonSimilarity/Representation/ScalarHilbertSeparability.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The countable coordinate Hilbert space used by the spectral model is separable, by approximation with its finite-coordinate vectors.

  1. instance OAI.KadisonSimilarity.scalarHilbertCoordinates_separable line 13