OAI/Analysis/Pureness/Quasitrace/QuasitraceBaseExtremal.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CuntzPureness.normalizedBaseQuasitraceCarrier line 10
  2. theorem OAI.CuntzPureness.mem_normalizedBaseQuasitraceCarrier line 13
  3. theorem OAI.CuntzPureness.isCompact_normalizedBaseQuasitraceCarrier line 22
  4. theorem OAI.CuntzPureness.isClosed_normalizedBaseQuasitraceCarrier line 26
  5. theorem OAI.CuntzPureness.convex_normalizedBaseQuasitraceCarrier line 30
  6. def OAI.CuntzPureness.additiveQuasitraceFunctions line 34
  7. lemma OAI.CuntzPureness.isClosed_additiveQuasitraceFunctions line 37
  8. lemma OAI.CuntzPureness.convex_additiveQuasitraceFunctions line 42
  9. theorem OAI.CuntzPureness.normalizedBaseQuasitraceCarrier_eq_closure_extremePoints line 49
  10. theorem OAI.CuntzPureness.normalizedQuasitrace_additive_of_base_extremePoints line 55
  11. theorem OAI.CuntzPureness.normalizedQuasitrace_trace_of_base_extremePoints line 64