OAI/Analysis/Pureness/Quasitrace/QuasitraceUltraproductAWEmbedding.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.CuntzPureness.boundedProductNontrivial line 16
  2. abbrev OAI.CuntzPureness.UltralimitAWCompletion line 28
  3. def OAI.CuntzPureness.ultralimitCompletionMap line 32
  4. lemma OAI.CuntzPureness.ultralimitCompletionMap_eq line 36
  5. def OAI.CuntzPureness.ultraproductAWEmbedding line 59
  6. lemma OAI.CuntzPureness.ultraproductAWEmbedding_map line 70
  7. lemma OAI.CuntzPureness.ultraproductAWEmbedding_injective line 75
  8. theorem OAI.CuntzPureness.ultralimitAWCompletion_annihilator line 83
  9. theorem OAI.CuntzPureness.ultralimitAWCompletion_finite line 90
  10. theorem OAI.CuntzPureness.filteredQuasitraceQuotient_finite line 96
  11. def OAI.CuntzPureness.ultralimitAWQuasitrace line 103
  12. lemma OAI.CuntzPureness.ultralimitAWQuasitrace_original line 108
  13. lemma OAI.CuntzPureness.ultralimitAWQuasitrace_faithful line 114
  14. lemma OAI.CuntzPureness.ultralimitAWQuasitrace_unit line 119