OAI/Analysis/Pureness/Comparison/SpatialTensorOperators.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CuntzComparison.SpatialHilbert line 14
2. def OAI.CuntzComparison.spatialTensorOp line 18
3. lemma OAI.CuntzComparison.spatialTensorOp_coe line 22
4. lemma OAI.CuntzComparison.spatialTensorOp_ext line 26
5. lemma OAI.CuntzComparison.spatialTensorOp_zero_left line 37
6. lemma OAI.CuntzComparison.spatialTensorOp_zero_right line 39
7. lemma OAI.CuntzComparison.spatialTensorOp_add_left line 41
8. lemma OAI.CuntzComparison.spatialTensorOp_add_right line 44
9. lemma OAI.CuntzComparison.spatialTensorOp_smul_left line 47
10. lemma OAI.CuntzComparison.spatialTensorOp_smul_right line 51
11. lemma OAI.CuntzComparison.spatialTensorOp_mul line 54
12. lemma OAI.CuntzComparison.completion_opNorm_le line 58
13. lemma OAI.CuntzComparison.spatialTensorOp_norm_le line 66
14. lemma OAI.CuntzComparison.spatialTensorOp_star line 71