OAI/Analysis/Pureness/Stabilization/CompactOperators.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CuntzTrace.rankOneGenerators line 14
  2. def OAI.CuntzTrace.finiteRankAlgebra line 16
  3. def OAI.CuntzTrace.compactOperatorAlgebra line 19
  4. instance OAI.CuntzTrace.compactOperatorAlgebra_closed line 22
  5. abbrev OAI.CuntzTrace.CompactOperators line 25
  6. instance OAI.CuntzTrace.(instance at line 27) line 27
  7. lemma OAI.CuntzTrace.rankOne_isCompact line 32
  8. lemma OAI.CuntzTrace.finiteRankAlgebra_compact line 37
  9. theorem OAI.CuntzTrace.compactOperators_areCompact line 52
  10. theorem OAI.CuntzTrace.rankOne_mem_compactOperators line 58
  11. abbrev OAI.CuntzTrace.StandardHilbert line 62
  12. abbrev OAI.CuntzTrace.StandardCompacts line 64