OAI/Analysis/BoundedHochschild/DiffuseSubfactor.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Countably generated diffuse subfactors obtained from matrix witnesses and small projections.

  1. theorem OAI.HochschildLocalization.exists_countable_matrix_witnesses line 23
  2. theorem OAI.HochschildLocalization.weakClosure_factor_of_matrix_witnesses line 65
  3. theorem OAI.HochschildLocalization.diffuse_of_small_projections line 142
  4. theorem OAI.HochschildLocalization.exists_small_projection_sequence line 170
  5. theorem OAI.HochschildLocalization.exists_countably_generated_diffuse_subfactor line 204