OAI/Analysis/Pureness/Tensor/SpatialHilbertBasisDensity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.spatialLeftVector line 13
2. lemma OAI.CuntzPureness.spatialLeftVector_apply line 17
3. lemma OAI.CuntzPureness.spatialTensorFamily_orthonormal line 22
4. theorem OAI.CuntzPureness.spatialTensorFamily_dense line 29
5. lemma OAI.CuntzPureness.groupDelta_orthonormal line 65
6. lemma OAI.CuntzPureness.groupDelta_dense line 69