OAI/Analysis/Pureness/Comparison/SpatialCompletion.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.CuntzComparison.stabilizationOperatorsCStar line 13
2. instance OAI.CuntzComparison.stabilizationOperatorsContinuousStar line 15
3. instance OAI.CuntzComparison.stabilizationOperatorsTopologicalRing line 17
4. def OAI.CuntzComparison.spatialRepresentation line 20
5. theorem OAI.CuntzComparison.spatialRepresentation_stage line 23
6. lemma OAI.CuntzComparison.spatialRepresentation_continuous line 27
7. theorem OAI.CuntzComparison.spatialRepresentation_norm line 35
8. theorem OAI.CuntzComparison.spatialRepresentation_isometry line 47
9. def OAI.CuntzComparison.spatialMatrixAlgebra line 51
10. lemma OAI.CuntzComparison.spatialRepresentation_mem line 54
11. theorem OAI.CuntzComparison.spatialRepresentation_range line 66