OAI/Analysis/Pureness/Quasitrace/NormalizedQuasitraceCarrier.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CuntzPureness.QuasitraceCoordinates line 11
2. def OAI.CuntzPureness.TwoQuasitrace.coordinates line 14
3. def OAI.CuntzPureness.normalizedQuasitraceCarrier line 17
4. lemma OAI.CuntzPureness.TwoQuasitrace.coordinates_mem line 21
5. def OAI.CuntzPureness.twoQuasitraceFromCoordinates line 25
6. lemma OAI.CuntzPureness.twoQuasitraceFromCoordinates_unit line 31
7. lemma OAI.CuntzPureness.range_normalized_quasitrace_coordinates line 35
8. lemma OAI.CuntzPureness.isClosed_normalizedQuasitraceCarrier line 45
9. lemma OAI.CuntzPureness.convex_normalizedQuasitraceCarrier line 54
10. theorem OAI.CuntzPureness.isCompact_normalizedQuasitraceCarrier line 66