OAI/Analysis/Pureness/Quasitrace/QuasitraceExtremalReduction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.additiveQuasitraceCoordinates line 10
2. lemma OAI.CuntzPureness.isClosed_additiveQuasitraceCoordinates line 14
3. lemma OAI.CuntzPureness.convex_additiveQuasitraceCoordinates line 21
4. theorem OAI.CuntzPureness.normalizedQuasitraceCarrier_eq_closure_extremePoints line 29
5. theorem OAI.CuntzPureness.exists_extreme_normalizedQuasitrace line 35
6. theorem OAI.CuntzPureness.normalizedQuasitrace_additive_of_extremePoints line 39