OAI/Analysis/KadisonKastler/SpatialVectorTransport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Pulling a cyclic separating vector back through an intertwining unitary

  1. theorem OAI.KadisonKastler.spatialVectorTransport_action line 19
  2. theorem OAI.KadisonKastler.spatialVectorTransport_state line 25
  3. theorem OAI.KadisonKastler.spatialVectorTransport_cyclic line 31
  4. theorem OAI.KadisonKastler.spatialVectorTransport_separating line 41