OAI/Analysis/Pureness/States/NormalizedMatrixStateUltraproduct.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CuntzPureness.matrixStateUnitValue line 13
  2. lemma OAI.CuntzPureness.matrixStateUnitValue_pos line 19
  3. def OAI.CuntzPureness.normalizedMatrixStatePositiveQuasitrace line 22
  4. lemma OAI.CuntzPureness.normalizedMatrixStatePositiveQuasitrace_unit line 28
  5. lemma OAI.CuntzPureness.normalizedMatrixStatePositiveQuasitrace_metricSize_add line 32
  6. lemma OAI.CuntzPureness.normalizedMatrixStatePositiveQuasitrace_sqrt_add line 39
  7. lemma OAI.CuntzPureness.normalizedMatrixStatePositiveQuasitrace_faithful line 46
  8. lemma OAI.CuntzPureness.normalizedMatrixStatePositiveQuasitrace_root_rank line 51
  9. abbrev OAI.CuntzPureness.NormalizedMatrixStateUltraproduct line 75
  10. abbrev OAI.CuntzPureness.NormalizedMatrixStateUltraAW line 80
  11. def OAI.CuntzPureness.normalizedMatrixStateUltraEmbedding line 85
  12. theorem OAI.CuntzPureness.normalizedMatrixStateUltra_finite_awstar line 89