OAI/Analysis/Pureness/Quasitrace/QuasitracePositiveMetricContinuity.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CuntzPureness.PositiveQuasitrace.exists_metric_delta_sqrt line 14
2. def OAI.CuntzPureness.PositiveQuasitrace.PositiveMetricPoint line 47
3. instance OAI.CuntzPureness.PositiveQuasitrace.positiveMetricPointPseudoMetric line 48
4. def OAI.CuntzPureness.PositiveQuasitrace.sqrtOnPositive line 50
5. lemma OAI.CuntzPureness.PositiveQuasitrace.sqrtOnPositive_uniformContinuous line 54
6. def OAI.CuntzPureness.PositiveQuasitrace.positiveCompletionValue line 63
7. lemma OAI.CuntzPureness.PositiveQuasitrace.positiveCompletionValue_coe line 66
8. lemma OAI.CuntzPureness.PositiveQuasitrace.positiveCompletionValue_nonneg line 72
9. lemma OAI.CuntzPureness.PositiveQuasitrace.positiveCompletionValue_continuous line 75