OAI/Analysis/KadisonKastler/StateGraphTransport.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Transporting the closed Tomita graph under a state isomorphism

  1. def OAI.KadisonKastler.stateGraphUnitary line 21
  2. theorem OAI.KadisonKastler.stateGraphUnitary_zero line 26
  3. theorem OAI.KadisonKastler.stateGraphUnitary_one line 33
  4. theorem OAI.KadisonKastler.stateGraphUnitary_vector line 41
  5. theorem OAI.KadisonKastler.stateGraphUnitary_mem line 63
  6. theorem OAI.KadisonKastler.stateGraphUnitary_symm_mem line 75
  7. theorem OAI.KadisonKastler.stateGraphProjection_transport line 90