OAI/Analysis/Pureness/Comparison/SpatialCompactTensor.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzComparison.spatialCompactAlgebra line 16
2. lemma OAI.CuntzComparison.spatialFinite_mem_compactAlgebra line 20
3. lemma OAI.CuntzComparison.spatialEntry_mem_matrixAlgebra line 30
4. def OAI.CuntzComparison.spatialTensorRight line 42
5. lemma OAI.CuntzComparison.spatialTensor_matrixUnitAlgebra line 49
6. theorem OAI.CuntzComparison.spatialTensor_compact_mem line 77
7. theorem OAI.CuntzComparison.spatialCompactAlgebra_eq_matrixAlgebra line 88
8. theorem OAI.CuntzComparison.spatialRepresentation_range_compact line 103