OAI/Analysis/Pureness/Tensor/SpatialCoordinateProjection.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.spatialRightOperator line 13
2. lemma OAI.CuntzPureness.spatialRightOperator_apply line 26
3. def OAI.CuntzPureness.spatialCoordinateProjection line 29
4. lemma OAI.CuntzPureness.spatialCoordinateProjection_norm_le line 32
5. lemma OAI.CuntzPureness.spatialCoordinateProjection_star line 38
6. lemma OAI.CuntzPureness.spatialCoordinateProjection_compl line 43
7. lemma OAI.CuntzPureness.spatialCoordinateProjection_disjoint line 49
8. lemma OAI.CuntzPureness.spatialCoordinateProjection_conjugate line 55
9. lemma OAI.CuntzPureness.spatialCoordinateProjection_tensor_zero line 63