OAI/Analysis/Pureness/Quasitrace/QuasitraceFunctionCarrier.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.complexQuasitraceCarrier line 10
2. lemma OAI.CuntzPureness.ComplexQuasitrace.mem_carrier line 20
3. def OAI.CuntzPureness.complexQuasitraceFromCarrier line 34
4. lemma OAI.CuntzPureness.range_complexQuasitrace_toFun line 46
5. lemma OAI.CuntzPureness.isClosed_forall_pointwise line 52
6. lemma OAI.CuntzPureness.isClosed_complexQuasitraceCarrier line 58
7. lemma OAI.CuntzPureness.convex_complexQuasitraceCarrier line 75