OAI/Analysis/FreeWords/GNSQuotient.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.KKUltraTrace.tracial_null_right line 36
  2. def OAI.KKUltraTrace.gnsQuotient line 49
  3. instance OAI.KKUltraTrace.gnsQuotient_closed line 52
  4. def OAI.KKUltraTrace.quotientOrder line 55
  5. def OAI.KKUltraTrace.quotientLE line 60
  6. def OAI.KKUltraTrace.quotientPreorder line 64
  7. theorem OAI.KKUltraTrace.quotientSOR line 68
  8. def OAI.KKUltraTrace.gnsExpectation line 73
  9. theorem OAI.KKUltraTrace.gnsExpectation_image line 76
  10. theorem OAI.KKUltraTrace.continuous_gnsExpectation line 80
  11. def OAI.KKUltraTrace.gnsQuotientState line 84
  12. theorem OAI.KKUltraTrace.gnsQuotientState_star_mul line 102
  13. theorem OAI.KKUltraTrace.gnsQuotientState_tracial line 108
  14. theorem OAI.KKUltraTrace.gnsQuotientState_faithful line 132
  15. theorem OAI.KKUltraTrace.gnsQuotient_has_faithful_trace line 151