OAI/Analysis/KadisonKastler/FaithfulCyclicTensor.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Tensoring the constructed faithful cyclic representation

The tensor representation is a restriction of countable amplification. Its defining isometry and its bounded weak continuity are concrete.

  1. def OAI.KadisonKastler.faithfulTensorEmbedding line 23
  2. theorem OAI.KadisonKastler.faithfulTensorEmbedding_tmul line 30
  3. theorem OAI.KadisonKastler.faithfulTensorEmbedding_projection line 41
  4. def OAI.KadisonKastler.faithfulTensorHom line 51
  5. theorem OAI.KadisonKastler.faithfulTensorHom_intertwines line 61
  6. theorem OAI.KadisonKastler.faithfulTensorHom_left line 69
  7. theorem OAI.KadisonKastler.faithfulTensorHom_right line 96
  8. theorem OAI.KadisonKastler.faithfulTensorHom_tendsto_weak line 121