OAI/Analysis/KadisonKastler/CommonRankFieldClosure.lean

GitHub source file

1 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. theorem OAI.KadisonKastler.commonRank_field_mem_of_closure line 34