OAI/Analysis/BoundedHochschild/CornerUnitaryExtension.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Extending corner unitaries by the identity on the complementary corner.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.corner_complement_left line 16
  2. lemma OAI.BoundedHochschild.KadisonRingrose.corner_complement_right line 21
  3. lemma OAI.BoundedHochschild.KadisonRingrose.cornerUnitaryExtension_mem line 26
  4. def OAI.BoundedHochschild.KadisonRingrose.cornerUnitaryExtension line 45
  5. lemma OAI.BoundedHochschild.KadisonRingrose.cornerUnitaryExtension_apply line 58