OAI/Analysis/Pureness/Tensor/SpatialCompletionIndependence.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.denseStarCompletionLinearEquiv line 16
2. lemma OAI.CuntzPureness.denseStarCompletionLinearEquiv_apply line 19
3. def OAI.CuntzPureness.denseStarCompletionEquiv line 23
4. lemma OAI.CuntzPureness.denseStarCompletionEquiv_apply line 44
5. lemma OAI.CuntzPureness.denseStarCompletionEquiv_norm line 48
6. def OAI.CuntzPureness.representedSpatialEquiv line 65
7. lemma OAI.CuntzPureness.representedSpatialEquiv_tensor line 71
8. lemma OAI.CuntzPureness.representedSpatialEquiv_norm line 76