OAI/Analysis/Pureness/States/FiniteFamilyCompletion.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CuntzPureness.CompatibleFiniteQuasitrace.CauchyLevel line 15
  2. def OAI.CuntzPureness.CompatibleFiniteQuasitrace.cauchyEmbedding line 18
  3. def OAI.CuntzPureness.CompatibleFiniteQuasitrace.cauchyValue line 21
  4. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.cauchyValue_embedding line 25
  5. def OAI.CuntzPureness.CompatibleFiniteQuasitrace.cauchyPositiveQuasitrace line 30
  6. def OAI.CuntzPureness.CompatibleFiniteQuasitrace.cauchyQuasitrace line 34
  7. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.cauchyQuasitrace_eq line 37
  8. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.cauchyValue_faithful line 41
  9. theorem OAI.CuntzPureness.CompatibleFiniteQuasitrace.cauchyLevel_finite line 45
  10. theorem OAI.CuntzPureness.CompatibleFiniteQuasitrace.cauchyLevel_annihilator line 49
  11. def OAI.CuntzPureness.CompatibleFiniteQuasitrace.cauchyInclusion line 55
  12. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.cauchyInclusion_embedding line 62
  13. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.cauchyInclusion_value line 66
  14. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.cauchyInclusion_isometry line 71
  15. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.cauchyInclusion_self line 75
  16. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.cauchyInclusion_trans line 85