OAI/Analysis/Pureness/States/FiniteFamilyCarrier.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CuntzPureness.FiniteQuasitraceCoordinates line 10
2. def OAI.CuntzPureness.CompatibleFiniteQuasitrace.coordinates line 13
3. def OAI.CuntzPureness.normalizedFiniteQuasitraceCarrier line 16
4. def OAI.CuntzPureness.finiteQuasitraceFromCoordinates line 21
5. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.coordinates_mem line 26
6. theorem OAI.CuntzPureness.isClosed_normalizedFiniteQuasitraceCarrier line 31
7. theorem OAI.CuntzPureness.convex_normalizedFiniteQuasitraceCarrier line 48
8. theorem OAI.CuntzPureness.isCompact_normalizedFiniteQuasitraceCarrier line 66