OAI/Analysis/Pureness/Quasitrace/QuasitraceNullIdeal.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.CuntzPureness.PositiveQuasitrace.cauchySequenceCompleteSpace line 14
2. instance OAI.CuntzPureness.PositiveQuasitrace.cauchySequenceCStarAlgebra line 16
3. def OAI.CuntzPureness.PositiveQuasitrace.nullSequenceIdeal line 18
4. lemma OAI.CuntzPureness.PositiveQuasitrace.nullSequenceIdeal_mem line 28
5. lemma OAI.CuntzPureness.PositiveQuasitrace.nullSequenceIdeal_star line 32
6. lemma OAI.CuntzPureness.PositiveQuasitrace.metricNull_isClosed line 39
7. lemma OAI.CuntzPureness.PositiveQuasitrace.nullSequenceIdeal_isClosed line 60
8. abbrev OAI.CuntzPureness.PositiveQuasitrace.CauchyQuotient line 67
9. def OAI.CuntzPureness.PositiveQuasitrace.cauchyQuotientMap line 69
10. lemma OAI.CuntzPureness.PositiveQuasitrace.cauchyQuotientMap_surjective line 72