OAI/Analysis/JiangSu/TensorProducts/SpatialCompactTensor.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UnitalTomsWinter.spatialCompactAlgebra line 45
2. lemma OAI.UnitalTomsWinter.spatialFinite_mem_compactAlgebra line 49
3. lemma OAI.UnitalTomsWinter.spatialEntry_mem_matrixAlgebra line 59
4. def OAI.UnitalTomsWinter.spatialTensorRight line 71
5. lemma OAI.UnitalTomsWinter.spatialTensor_matrixUnitAlgebra line 78
6. theorem OAI.UnitalTomsWinter.spatialTensor_compact_mem line 106
7. theorem OAI.UnitalTomsWinter.spatialCompactAlgebra_eq_matrixAlgebra line 117
8. theorem OAI.UnitalTomsWinter.spatialRepresentation_range_compact line 132