OAI/Analysis/KadisonKastler/IsometricCornerAlgebra.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The von Neumann algebra on a reducing isometric range

  1. def OAI.KadisonKastler.rangeCompression line 19
  2. theorem OAI.KadisonKastler.rangeCompression_intertwines_apply line 22
  3. def OAI.KadisonKastler.rangeCompressionStarHom line 32
  4. theorem OAI.KadisonKastler.rangeCompressionStarHom_intertwines line 57
  5. theorem OAI.KadisonKastler.rangeProjection_commutes_commutant line 67
  6. def OAI.KadisonKastler.isometricCornerAlgebra line 71
  7. theorem OAI.KadisonKastler.mem_isometricCornerAlgebra_iff line 75