OAI/Analysis/Pureness/States/FiniteFamilyPullback.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CuntzPureness.matrixMap_inclusion line 13
2. lemma OAI.CuntzPureness.matrixMap_scalarMatrix line 22
3. def OAI.CuntzPureness.CompatibleFiniteQuasitrace.comap line 31
4. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.comap_monotone line 38
5. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.comap_base line 45
6. def OAI.CuntzPureness.CompatibleFiniteQuasitrace.scale line 50
7. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.scale_monotone line 54
8. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.scale_unit line 63
9. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.scale_base line 69
10. theorem OAI.CuntzPureness.CompatibleFiniteQuasitrace.normalized_comap_mem line 72