OAI/Analysis/JiangSu/TraceCone/CuntzDenseMaps.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.TraceCone.starHom_continuous line 16
  2. theorem OAI.TraceCone.Positive.map_cut line 23
  3. theorem OAI.TraceCone.cuntzClass_maps_eq_of_dense line 30
  4. def OAI.TraceCone.matrixParityEmbedding line 70
  5. def OAI.TraceCone.matrixParity line 74
  6. lemma OAI.TraceCone.matrixParity_embedding line 77
  7. lemma OAI.TraceCone.matrixParity_stage line 95
  8. theorem OAI.TraceCone.matrixLimit_maps_eq line 101
  9. theorem OAI.TraceCone.matrixParity_cuntzClass line 118
  10. instance OAI.TraceCone.CuntzClass.(instance at line 129) line 129
  11. lemma OAI.TraceCone.CuntzClass.zero_mk line 130
  12. theorem OAI.TraceCone.CuntzClass.matrixAdd_zero line 132
  13. theorem OAI.TraceCone.CuntzClass.zero_matrixAdd line 141
  14. structure OAI.TraceCone.PositiveCore line 160
  15. def OAI.TraceCone.matrixPositiveCore line 166
  16. def OAI.TraceCone.PositiveCore.prod line 177
  17. theorem OAI.TraceCone.PositiveCore.maps_eq line 190
  18. theorem OAI.TraceCone.matrixPositiveCore_common line 195