OAI/Analysis/Pureness/Cuntz/FiniteMatrixLimit.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CuntzPureness.MatrixStage line 8
  2. def OAI.CuntzPureness.matrixConnecting line 9
  3. instance OAI.CuntzPureness.matrixDirectedSystem line 12
  4. abbrev OAI.CuntzPureness.FiniteMatrixLimit line 16
  5. def OAI.CuntzPureness.finiteMatrixInclude line 18
  6. lemma OAI.CuntzPureness.finiteMatrixInclude_injective line 26
  7. lemma OAI.CuntzPureness.finiteMatrixInclude_corner line 29
  8. def OAI.CuntzPureness.finiteMatrixNorm line 35
  9. lemma OAI.CuntzPureness.finiteMatrixNorm_include line 39
  10. def OAI.CuntzPureness.finiteMatrixGroupNorm line 42
  11. instance OAI.CuntzPureness.finiteMatrixNormedAddCommGroup line 64
  12. instance OAI.CuntzPureness.finiteMatrixTopology line 67
  13. lemma OAI.CuntzPureness.finiteMatrixInclude_norm line 70
  14. lemma OAI.CuntzPureness.finiteMatrixInclude_isometry line 73
  15. instance OAI.CuntzPureness.finiteMatrixNonUnitalNormedRing line 76
  16. instance OAI.CuntzPureness.finiteMatrixModule line 85
  17. instance OAI.CuntzPureness.finiteMatrixNormedSpace line 109
  18. instance OAI.CuntzPureness.finiteMatrixStarRing line 118
  19. instance OAI.CuntzPureness.finiteMatrixCStarRing line 122