OAI/Analysis/Pureness/Quasitrace/QuasitraceQuotientRootCauchy.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CuntzPureness.PositiveQuasitrace.quotientValue_neg line 15
2. lemma OAI.CuntzPureness.PositiveQuasitrace.quotientValue_cfc_sub line 24
3. lemma OAI.CuntzPureness.PositiveQuasitrace.quotientMetricSize_positive_cube_le line 33
4. lemma OAI.CuntzPureness.PositiveQuasitrace.quotient_root_eq_cfc line 45
5. lemma OAI.CuntzPureness.PositiveQuasitrace.quotient_root_value_sub line 53
6. lemma OAI.CuntzPureness.PositiveQuasitrace.quotient_roots_metricCauchy line 63
7. lemma OAI.CuntzPureness.PositiveQuasitrace.exists_quotient_root_limit line 109