OAI/Analysis/Pureness/Stabilization/MatrixLimitLift.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CuntzTrace.finiteMatrixSubalgebra line 11
  2. def OAI.CuntzTrace.finiteMatrixStage line 14
  3. lemma OAI.CuntzTrace.finiteMatrixStage_surjective line 17
  4. lemma OAI.CuntzTrace.finiteMatrixSubalgebra_dense line 22
  5. def OAI.CuntzTrace.finiteMatrixRepresentative line 29
  6. lemma OAI.CuntzTrace.finiteMatrixRepresentative_spec line 32
  7. def OAI.CuntzTrace.finiteMatrixLiftValue line 39
  8. lemma OAI.CuntzTrace.finiteMatrixLiftValue_eq line 43
  9. lemma OAI.CuntzTrace.finiteMatrixLiftValue_stage line 55
  10. lemma OAI.CuntzTrace.finiteMatrix_common_stage line 59
  11. def OAI.CuntzTrace.finiteMatrixLift line 67
  12. lemma OAI.CuntzTrace.finiteMatrixLift_norm_le line 90
  13. def OAI.CuntzTrace.matrixLimitLift line 96
  14. theorem OAI.CuntzTrace.matrixLimitLift_stage line 100