OAI/Analysis/KadisonKastler/TwoStateCornerEmbedding.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Isometric embeddings of the two diagonal state spaces

  1. def OAI.KadisonKastler.twoStateCornerEmbedding line 16
  2. theorem OAI.KadisonKastler.twoStateCornerEmbedding_fst_zero line 28
  3. theorem OAI.KadisonKastler.twoStateCornerEmbedding_snd_zero line 32
  4. theorem OAI.KadisonKastler.twoStateCornerEmbedding_fst_one line 36
  5. theorem OAI.KadisonKastler.twoStateCornerEmbedding_snd_one line 40
  6. def OAI.KadisonKastler.twoStateVectorAt line 43
  7. theorem OAI.KadisonKastler.twoStateCornerEmbedding_vector line 45