OAI/Analysis/Pureness/States/FiniteFamilyBaseCarrier.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CuntzPureness.CompatibleFiniteQuasitrace.toTwoQuasitrace line 12
  2. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.toTwoQuasitrace_unit line 18
  3. def OAI.CuntzPureness.finiteQuasitraceBaseMap line 23
  4. lemma OAI.CuntzPureness.continuous_finiteQuasitraceBaseMap line 29
  5. def OAI.CuntzPureness.normalizedFiniteBaseQuasitraceCarrier line 34
  6. theorem OAI.CuntzPureness.mem_normalizedFiniteBaseQuasitraceCarrier line 37
  7. theorem OAI.CuntzPureness.isCompact_normalizedFiniteBaseQuasitraceCarrier line 48
  8. theorem OAI.CuntzPureness.convex_normalizedFiniteBaseQuasitraceCarrier line 52
  9. theorem OAI.CuntzPureness.normalizedFiniteBaseQuasitraceCarrier_subset line 56
  10. theorem OAI.CuntzPureness.normalizedFiniteBaseQuasitraceCarrier_eq_closure_extremePoints line 63
  11. theorem OAI.CuntzPureness.finiteQuasitrace_additive_of_base_extremePoints line 69