OAI/Analysis/KadisonKastler/ComplementaryCornerUnitary.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Joining unitaries on complementary projection corners

The two corner conjugations used in state homogeneity join to one actual unitary. Its two compressions remain exactly the specified corner maps.

  1. theorem OAI.KadisonKastler.complementary_corner_sum_unitary line 21
  2. def OAI.KadisonKastler.complementaryCornerUnitary line 41
  3. theorem OAI.KadisonKastler.cornerUnitary_supports line 46
  4. theorem OAI.KadisonKastler.complementaryCornerUnitary_compressions line 53
  5. theorem OAI.KadisonKastler.complementary_corner_conjugation line 69