OAI/Analysis/Pureness/Comparison/SpatialIdentification.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.CuntzComparison.spatialCompactAlgebra_closed line 14
  2. abbrev OAI.CuntzComparison.SpatialStabilization line 17
  3. instance OAI.CuntzComparison.(instance at line 19) line 19
  4. def OAI.CuntzComparison.spatialRepresentationInto line 22
  5. def OAI.CuntzComparison.spatialEquiv line 33
  6. theorem OAI.CuntzComparison.spatialEquiv_norm line 43
  7. def OAI.CuntzComparison.spatialStage line 46
  8. lemma OAI.CuntzComparison.spatialStage_eq_equiv line 49
  9. theorem OAI.CuntzComparison.spatialStage_coe line 52
  10. theorem OAI.CuntzComparison.spatialStage_isometry line 56
  11. theorem OAI.CuntzComparison.transport_full_corner line 62
  12. theorem OAI.CuntzComparison.spatialStage_full_corner line 75
  13. theorem OAI.CuntzComparison.cuntzSubequiv_reflect_spatial line 84
  14. def OAI.CuntzComparison.TracialState.spatialEquiv line 89