OAI/Analysis/KadisonKastler/VonNeumannProjectionCommutation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Testing commutation on the projections of a von Neumann algebra

Finite spectral sums approximate every self-adjoint element in norm. Their commutation identities pass to the limit, and real/imaginary decomposition gives the identity on the whole algebra.

  1. theorem OAI.KadisonKastler.commutes_vonNeumann_of_projections line 21
  2. theorem OAI.KadisonKastler.mem_commutant_of_commutes_projections line 56