OAI/Analysis/KadisonKastler/CommonRankSourceModel.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Actual rank fields of a represented bicommutant member

Kaplansky approximation on the original representation, transported through the constructed unitary, places the rank fields in the corresponding fiber bicommutants. The common source may be larger than the algebra being closed.

  1. abbrev OAI.KadisonKastler.CommonRankSpace line 30
  2. abbrev OAI.KadisonKastler.commonRankSourceMeasure line 34
  3. def OAI.KadisonKastler.commonRankFiberAlgebra line 38
  4. theorem OAI.KadisonKastler.commonRankFiberAlgebra_le_commutant line 45
  5. theorem OAI.KadisonKastler.commonRankSpace_separable line 56