OAI/Analysis/Pureness/Comparison/SpatialFiniteMatrices.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CuntzComparison.StabilizationHilbert line 14
  2. abbrev OAI.CuntzComparison.StabilizationOperators line 16
  3. def OAI.CuntzComparison.spatialEntry line 19
  4. lemma OAI.CuntzComparison.spatialEntry_zero line 22
  5. lemma OAI.CuntzComparison.spatialEntry_add line 23
  6. lemma OAI.CuntzComparison.spatialEntry_smul line 26
  7. lemma OAI.CuntzComparison.spatialEntry_star line 29
  8. lemma OAI.CuntzComparison.spatialEntry_mul line 34
  9. lemma OAI.CuntzComparison.spatialEntry_sum line 44
  10. def OAI.CuntzComparison.spatialMatrixSum line 51
  11. lemma OAI.CuntzComparison.spatialMatrixSum_star line 53
  12. lemma OAI.CuntzComparison.spatialMatrixSum_mul line 60
  13. def OAI.CuntzComparison.spatialFiniteValue line 71
  14. lemma OAI.CuntzComparison.spatialFiniteValue_star line 74
  15. lemma OAI.CuntzComparison.spatialFiniteValue_mul line 78
  16. def OAI.CuntzComparison.spatialFinite line 82
  17. lemma OAI.CuntzComparison.spatialFinite_coefficient line 90
  18. theorem OAI.CuntzComparison.spatialFinite_injective line 96
  19. theorem OAI.CuntzComparison.spatialFinite_isometry line 106
  20. lemma OAI.CuntzComparison.spatialFinite_successor line 110
  21. theorem OAI.CuntzComparison.spatialFinite_compatible line 114