OAI/Analysis/Pureness/Quasitrace/QuasitraceQuotientFunctor.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CuntzPureness.PositiveQuasitrace.metricSize_map_of_positive_compatible line 17
2. lemma OAI.CuntzPureness.PositiveQuasitrace.distance_map_of_positive_compatible line 28
3. def OAI.CuntzPureness.PositiveQuasitrace.cauchySequenceFunctor line 32
4. lemma OAI.CuntzPureness.PositiveQuasitrace.cauchySequenceFunctor_rel line 45
5. def OAI.CuntzPureness.PositiveQuasitrace.quotientFunctor line 54
6. lemma OAI.CuntzPureness.PositiveQuasitrace.quotientFunctor_map line 84
7. lemma OAI.CuntzPureness.PositiveQuasitrace.quotientFunctor_embedding line 88
8. lemma OAI.CuntzPureness.PositiveQuasitrace.quotientFunctor_value line 94
9. lemma OAI.CuntzPureness.PositiveQuasitrace.quotientFunctor_metricSize line 103
10. lemma OAI.CuntzPureness.PositiveQuasitrace.quotientFunctor_distance line 108
11. lemma OAI.CuntzPureness.PositiveQuasitrace.quotientFunctor_injective line 115
12. lemma OAI.CuntzPureness.PositiveQuasitrace.quotientFunctor_isometry line 121