OAI/Analysis/Pureness/States/FiniteFamilyTraceReduction.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.CompatibleFiniteQuasitrace.originalEmbedding line 15
2. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.cauchyValue_original line 18
3. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.completedFamily_original line 22
4. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.originalEmbedding_cover line 26
5. theorem OAI.CuntzPureness.CompatibleFiniteQuasitrace.extreme_cauchyLevel_central_projection line 37
6. theorem OAI.CuntzPureness.CompatibleFiniteQuasitrace.extreme_cauchy_trace_agrees line 51
7. theorem OAI.CuntzPureness.CompatibleFiniteQuasitrace.extreme_original_additive_of_cauchy_trace line 63
8. theorem OAI.CuntzPureness.finiteBase_extreme_additive_of_cauchy_traces line 72