OAI/Analysis/Commutator/HilbertModuleSchroederBernstein.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Kadison.HilbertModuleSB.intertwinerAlgebra line 26
  2. lemma OAI.Kadison.HilbertModuleSB.mem_intertwinerAlgebra line 33
  3. lemma OAI.Kadison.HilbertModuleSB.left_mem line 41
  4. lemma OAI.Kadison.HilbertModuleSB.right_mem line 44
  5. def OAI.Kadison.HilbertModuleSB.offDiagonal line 47
  6. lemma OAI.Kadison.HilbertModuleSB.offDiagonal_apply line 50
  7. lemma OAI.Kadison.HilbertModuleSB.offDiagonal_initial line 55
  8. lemma OAI.Kadison.HilbertModuleSB.offDiagonal_right line 68
  9. lemma OAI.Kadison.HilbertModuleSB.offDiagonal_left line 73
  10. lemma OAI.Kadison.HilbertModuleSB.offDiagonal_mem line 78
  11. lemma OAI.Kadison.HilbertModuleSB.subEquivalent_of_embedding line 86
  12. def OAI.Kadison.HilbertModuleSB.offDiagonalReverse line 97
  13. lemma OAI.Kadison.HilbertModuleSB.offDiagonalReverse_apply line 100
  14. lemma OAI.Kadison.HilbertModuleSB.offDiagonalReverse_initial line 105
  15. lemma OAI.Kadison.HilbertModuleSB.offDiagonalReverse_left line 118
  16. lemma OAI.Kadison.HilbertModuleSB.offDiagonalReverse_right line 123
  17. lemma OAI.Kadison.HilbertModuleSB.offDiagonalReverse_mem line 128
  18. lemma OAI.Kadison.HilbertModuleSB.subEquivalent_of_reverse_embedding line 136
  19. lemma OAI.Kadison.HilbertModuleSB.link_component_isometry line 147
  20. lemma OAI.Kadison.HilbertModuleSB.link_component_coisometry line 156
  21. theorem OAI.Kadison.HilbertModuleSB.exists_unitary_of_embeddings line 176