OAI/Analysis/Pureness/States/OriginalScalarNuclearTensor.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CuntzPureness.originalScalarSpatialHom_norm_eq_AW line 18
2. def OAI.CuntzPureness.originalScalarNuclearEquiv line 23
3. lemma OAI.CuntzPureness.originalScalarNuclearEquiv_tensor line 32
4. lemma OAI.CuntzPureness.originalScalarNuclearEquiv_norm line 37
5. def OAI.CuntzPureness.originalScalarSpatialAWEmbedding line 41
6. lemma OAI.CuntzPureness.originalScalarSpatialAWEmbedding_tensor line 46
7. lemma OAI.CuntzPureness.originalScalarSpatialAWEmbedding_isometry line 52
8. lemma OAI.CuntzPureness.originalScalarSpatialAWEmbedding_left line 58
9. lemma OAI.CuntzPureness.originalScalarSpatialAWEmbedding_right line 69