OAI/Analysis/KadisonKastler/SpatialProjectionCorners.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Spatial derivations and off-diagonal projection corners

  1. theorem OAI.KadisonKastler.boundedSpatialResiduals_preserves_commutant line 14
  2. theorem OAI.KadisonKastler.CuntzFamily.offDiagonal_mem_of_preserves line 32
  3. theorem OAI.KadisonKastler.CuntzFamily.firstRange_commutes_of_corner_zero line 41