OAI/Analysis/Pureness/Tensor/OriginalFreeGroupSpatialTensor.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CuntzPureness.originalFreeGroupSpatialHom line 12
  2. lemma OAI.CuntzPureness.originalFreeGroupSpatialHom_injective line 17
  3. lemma OAI.CuntzPureness.originalFreeGroupSpatialHom_tmul_norm line 21
  4. abbrev OAI.CuntzPureness.OriginalFreeGroupSpatialCompletion line 28
  5. def OAI.CuntzPureness.originalFreeGroupSpatialCompletionMap line 31
  6. lemma OAI.CuntzPureness.originalFreeGroupSpatialCompletionMap_injective line 34
  7. lemma OAI.CuntzPureness.originalFreeGroupSpatialCompletionMap_dense line 39
  8. abbrev OAI.CuntzPureness.OriginalFreeGroupAWImage line 46
  9. def OAI.CuntzPureness.originalFreeGroupAWImageMap line 51
  10. lemma OAI.CuntzPureness.originalFreeGroupAWImageMap_injective line 54
  11. lemma OAI.CuntzPureness.originalFreeGroupAWImageMap_dense line 59
  12. lemma OAI.CuntzPureness.originalFreeGroupSpatialHom_norm_eq_AW line 67
  13. def OAI.CuntzPureness.originalFreeGroupNuclearEquiv line 72
  14. def OAI.CuntzPureness.originalFreeGroupSpatialAWEmbedding line 81
  15. lemma OAI.CuntzPureness.originalFreeGroupSpatialAWEmbedding_tensor line 86
  16. lemma OAI.CuntzPureness.originalFreeGroupSpatialAWEmbedding_isometry line 98