OAI/Analysis/Pureness/Quasitrace/QuasitraceQuotientOrder.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.CuntzPureness.PositiveQuasitrace.cauchyQuotientPartialOrder line 14
2. instance OAI.CuntzPureness.PositiveQuasitrace.cauchyQuotientStarOrderedRing line 15
3. lemma OAI.CuntzPureness.PositiveQuasitrace.exists_positive_quotient_representative line 17
4. lemma OAI.CuntzPureness.PositiveQuasitrace.quotientValue_nonneg line 24
5. lemma OAI.CuntzPureness.PositiveQuasitrace.cauchyValue_positive_mono line 28
6. lemma OAI.CuntzPureness.PositiveQuasitrace.quotientValue_positive_mono line 45