OAI/Analysis/Pureness/States/FiniteFamilyMatrixCompletion.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.cauchyInclusion_unit_corner line 14
2. def OAI.CuntzPureness.CompatibleFiniteQuasitrace.cauchyMatrixLeg line 26
3. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.cauchyMatrixLeg_orthogonal line 29
4. def OAI.CuntzPureness.CompatibleFiniteQuasitrace.cauchyMatrixLift line 44
5. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.cauchyMatrixLeg_inclusion line 48
6. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.cauchyMatrixLift_inclusion line 55
7. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.cauchyMatrixLift_scalar_one line 61
8. def OAI.CuntzPureness.CompatibleFiniteQuasitrace.completedFamily line 70
9. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.completedFamily_monotone line 79
10. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.completedFamily_base line 95
11. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.completedFamily_unit line 100