OAI/Analysis/KadisonKastler/SpatialDerivationClosure.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Spatial derivations pass to the bicommutant

Kaplansky's constructed bounded net transfers commutator membership to the represented closure. Central projections in that closure therefore commute with the spatial implementer.

  1. theorem OAI.KadisonKastler.spatial_commutator_mem_generated_contraction line 23
  2. theorem OAI.KadisonKastler.spatial_commutator_mem_generated line 44
  3. theorem OAI.KadisonKastler.spatial_commutator_central_projection line 62