OAI/Analysis/Pureness/Completion/CompletedSpatialTensorMap.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CuntzPureness.algebraicStarTensorMap line 20
  2. lemma OAI.CuntzPureness.algebraicStarTensorMap_eq line 31
  3. abbrev OAI.CuntzPureness.spatialCompletionMap line 34
  4. def OAI.CuntzPureness.completedSpatialTensorMap line 45
  5. lemma OAI.CuntzPureness.completedSpatialTensorMap_tensor line 56
  6. lemma OAI.CuntzPureness.completedSpatialTensorMap_norm_le line 61
  7. lemma OAI.CuntzPureness.completedSpatialTensorMap_unique line 65
  8. lemma OAI.CuntzPureness.completedSpatialTensorMap_denseRange line 72
  9. lemma OAI.CuntzPureness.completedSpatialTensorMap_surjective line 84
  10. lemma OAI.CuntzPureness.completedSpatialTensorMap_isometry line 92