OAI/Analysis/FreeWords/BicommutantTrace.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KKUltraTrace.bicommutantAlg line 16
  2. theorem OAI.KKUltraTrace.coe_bicommutantAlg line 19
  3. instance OAI.KKUltraTrace.bicommutantAlg_closed line 24
  4. def OAI.KKUltraTrace.biOrder line 29
  5. def OAI.KKUltraTrace.biLE line 34
  6. def OAI.KKUltraTrace.biPreorder line 39
  7. theorem OAI.KKUltraTrace.biSOR line 44
  8. theorem OAI.KKUltraTrace.subset_bicommutantAlg line 49
  9. theorem OAI.KKUltraTrace.bicommutant_eval_closed line 55
  10. def OAI.KKUltraTrace.bicommutantState line 72
  11. theorem OAI.KKUltraTrace.bicommutantState_apply line 89
  12. theorem OAI.KKUltraTrace.trace_relation_extend line 92
  13. theorem OAI.KKUltraTrace.bicommutantState_tracial line 101