OAI/Analysis/Pureness/States/FiniteFamilyNuclearSpatial.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CuntzPureness.CompatibleFiniteQuasitrace.OriginalFreeGroupAWImage line 15
2. def OAI.CuntzPureness.CompatibleFiniteQuasitrace.originalFreeGroupAWImageMap line 20
3. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.originalFreeGroupAWImageMap_injective line 23
4. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.originalFreeGroupAWImageMap_dense line 28
5. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.originalFreeGroupSpatialHom_norm_eq_AW line 36
6. def OAI.CuntzPureness.CompatibleFiniteQuasitrace.originalFreeGroupNuclearEquiv line 41
7. def OAI.CuntzPureness.CompatibleFiniteQuasitrace.originalFreeGroupSpatialAWEmbedding line 50
8. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.originalFreeGroupSpatialAWEmbedding_tensor line 55
9. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.originalFreeGroupSpatialAWEmbedding_isometry line 67