OAI/Analysis/Pureness/States/FiniteFamilyNuclearTrace.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.cauchyLevel_zero_nontrivial line 19
2. theorem OAI.CuntzPureness.CompatibleFiniteQuasitrace.cauchyLevel_has_tracialState line 30
3. theorem OAI.CuntzPureness.nuclear_finiteBase_extreme_additive line 42
4. theorem OAI.CuntzPureness.nuclear_finiteFamily_original_additive line 47
5. theorem OAI.CuntzPureness.nuclear_normalizedRegularizedState_additive line 54
6. theorem OAI.CuntzPureness.nuclear_regularizedState_agreeing_trace line 62