OAI/Analysis/Pureness/Stabilization/MatrixLimit.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzTrace.matrixUnion line 10
2. def OAI.CuntzTrace.matrixLimitAlgebra line 28
3. instance OAI.CuntzTrace.matrixLimitAlgebra_closed line 31
4. abbrev OAI.CuntzTrace.MatrixLimit line 34
5. instance OAI.CuntzTrace.(instance at line 36) line 36
6. def OAI.CuntzTrace.matrixLimitStage line 40
7. lemma OAI.CuntzTrace.matrixLimitStage_norm line 48
8. lemma OAI.CuntzTrace.matrixLimitStage_isometry line 51
9. lemma OAI.CuntzTrace.matrixLimitStage_compatible line 54
10. theorem OAI.CuntzTrace.matrixLimit_finite_approximation line 58