OAI/Analysis/KadisonKastler/SpatialConjugacyTransport.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Transporting an implementer through Hilbert coordinates

  1. def OAI.KadisonKastler.spatialTransportUnitary line 15
  2. theorem OAI.KadisonKastler.coe_spatialTransportUnitary line 19
  3. theorem OAI.KadisonKastler.norm_spatialTransportUnitary_sub_one line 23
  4. theorem OAI.KadisonKastler.unitaryConj_spatialTransport line 29
  5. theorem OAI.KadisonKastler.Conjugates.spatialTransport line 35
  6. theorem OAI.KadisonKastler.spatialTransportAlgebra_symm line 45
  7. theorem OAI.KadisonKastler.exists_bounded_conjugacy_of_spatialTransport line 53