OAI/Analysis/Pureness/States/ScalarTracialUltraproductTrace.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CuntzPureness.scalarMatrixPositiveTrace_eq_state line 10
  2. instance OAI.CuntzPureness.scalarMatrixUltraPartialOrder line 20
  3. instance OAI.CuntzPureness.scalarMatrixUltraStarOrderedRing line 22
  4. lemma OAI.CuntzPureness.scalarFilteredQuotientMap_apply line 25
  5. def OAI.CuntzPureness.scalarMatrixUltraValue line 31
  6. lemma OAI.CuntzPureness.scalarMatrixUltraValue_map line 37
  7. lemma OAI.CuntzPureness.scalarMatrixUltraValue_tendsto line 43
  8. lemma OAI.CuntzPureness.scalarMatrixUltraValue_add line 51
  9. lemma OAI.CuntzPureness.scalarMatrixUltraValue_smul line 63
  10. lemma OAI.CuntzPureness.scalarMatrixUltraValue_tracial line 73
  11. lemma OAI.CuntzPureness.scalarMatrixUltraValue_unit line 86
  12. lemma OAI.CuntzPureness.scalarMatrixUltraValue_square_nonneg line 90
  13. lemma OAI.CuntzPureness.scalarMatrixUltraValue_square_eq_zero line 100
  14. def OAI.CuntzPureness.scalarMatrixUltraLinear line 117
  15. def OAI.CuntzPureness.scalarMatrixUltraTracialState line 122
  16. lemma OAI.CuntzPureness.scalarMatrixUltraTracialState_faithful line 137