OAI/Analysis/JiangSu/TensorProducts/SpatialIdentification.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.UnitalTomsWinter.spatialCompactAlgebra_closed line 50
  2. abbrev OAI.UnitalTomsWinter.SpatialStabilization line 53
  3. instance OAI.UnitalTomsWinter.(instance at line 55) line 55
  4. def OAI.UnitalTomsWinter.spatialRepresentationInto line 58
  5. def OAI.UnitalTomsWinter.spatialEquiv line 69
  6. theorem OAI.UnitalTomsWinter.spatialEquiv_norm line 79
  7. def OAI.UnitalTomsWinter.spatialStage line 82
  8. lemma OAI.UnitalTomsWinter.spatialStage_eq_equiv line 85
  9. theorem OAI.UnitalTomsWinter.spatialStage_coe line 88
  10. theorem OAI.UnitalTomsWinter.spatialStage_isometry line 92
  11. theorem OAI.UnitalTomsWinter.transport_full_corner line 98
  12. theorem OAI.UnitalTomsWinter.spatialStage_full_corner line 111
  13. theorem OAI.UnitalTomsWinter.cuntzSubequiv_reflect_spatial line 120
  14. def OAI.UnitalTomsWinter.TracialState.spatialEquiv line 125
  15. def OAI.Pureness.completedSpatialEquiv line 153
  16. theorem OAI.Pureness.completedSpatialEquiv_stage line 156
  17. theorem OAI.Pureness.completedSpatialEquiv_norm line 164
  18. theorem OAI.Pureness.completedSpatialEquiv_cut line 171
  19. def OAI.Pureness.TracialState.toShared line 177
  20. theorem OAI.Pureness.TracialState.source_gns_injective line 182
  21. def OAI.Pureness.TracialState.completedSpatialEquiv line 189