OAI/Analysis/Pureness/States/FiniteFamilyAWPositive.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.CuntzPureness.CompatibleFiniteQuasitrace.matrixUltraAWNontrivial line 15
2. abbrev OAI.CuntzPureness.CompatibleFiniteQuasitrace.matrixUltralimitPositive line 22
3. abbrev OAI.CuntzPureness.CompatibleFiniteQuasitrace.matrixUltralimitTriangle line 25
4. abbrev OAI.CuntzPureness.CompatibleFiniteQuasitrace.matrixUltralimitSqrt line 29
5. abbrev OAI.CuntzPureness.CompatibleFiniteQuasitrace.matrixAWPositive line 33
6. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.matrixAWPositive_complex line 37
7. abbrev OAI.CuntzPureness.CompatibleFiniteQuasitrace.matrixAWPositive_triangle line 40
8. abbrev OAI.CuntzPureness.CompatibleFiniteQuasitrace.matrixAWPositive_sqrt line 44
9. def OAI.CuntzPureness.CompatibleFiniteQuasitrace.matrixFinOneAW line 48
10. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.matrixFinOneAW_complex line 51
11. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.matrixFinOneAW_positive line 61