OAI/Analysis/Pureness/Quasitrace/QuasitraceNullApproximateUnit.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.PositiveQuasitrace.nullSequenceStarAlgebra line 13
2. instance OAI.CuntzPureness.PositiveQuasitrace.nullSequenceStarAlgebraCompleteSpace line 24
3. instance OAI.CuntzPureness.PositiveQuasitrace.nullSequenceStarAlgebraCStar line 26
4. instance OAI.CuntzPureness.PositiveQuasitrace.cauchySequencePartialOrder line 29
5. instance OAI.CuntzPureness.PositiveQuasitrace.cauchySequenceStarOrderedRing line 31
6. instance OAI.CuntzPureness.PositiveQuasitrace.nullSequencePartialOrder line 33
7. instance OAI.CuntzPureness.PositiveQuasitrace.nullSequenceStarOrderedRing line 35
8. def OAI.CuntzPureness.PositiveQuasitrace.nullSequenceInclusion line 43
9. lemma OAI.CuntzPureness.PositiveQuasitrace.nullSequenceInclusion_nonneg line 51
10. lemma OAI.CuntzPureness.PositiveQuasitrace.cauchySequence_norm_one_sub line 60
11. lemma OAI.CuntzPureness.PositiveQuasitrace.exists_null_contraction line 67