OAI/Analysis/Pureness/Comparison/SpatialTrace.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.CuntzComparison.(instance at line 14) line 14
2. instance OAI.CuntzComparison.(instance at line 15) line 15
3. def OAI.CuntzComparison.spatialInverse line 17
4. lemma OAI.CuntzComparison.spatialInverse_stage line 20
5. def OAI.CuntzComparison.TracialState.spatialTrace line 24
6. lemma OAI.CuntzComparison.spatialInverse_positive_stage line 27
7. theorem OAI.CuntzComparison.TracialState.spatialTrace_stage line 31
8. theorem OAI.CuntzComparison.TracialState.spatialTrace_rank_stage line 38
9. theorem OAI.CuntzComparison.TracialState.spatialTrace_rank_eq_supportMass line 48