OAI/Analysis/Pureness/States/FiniteFamilyAmplification.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.CompatibleFiniteQuasitrace.matrixAmplificationRaw line 13
2. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.matrixAmplificationRaw_base line 21
3. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.matrixAmplificationRaw_monotone line 26
4. def OAI.CuntzPureness.CompatibleFiniteQuasitrace.matrixAmplification line 34
5. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.matrixAmplification_level line 37
6. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.matrixAmplification_base line 41
7. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.matrixAmplification_monotone line 47
8. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.matrixAmplification_unit line 55
9. theorem OAI.CuntzPureness.CompatibleFiniteQuasitrace.level_additive_of_matrix_nuclear line 69