OAI/Analysis/BoundedHochschild/UnitaryPrefixDeletion.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Deleting a vertex from a prefix transport changes its cutoff exactly when that vertex was already transported.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.unitaryPrefix_removeNth_before line 14
  2. lemma OAI.BoundedHochschild.KadisonRingrose.unitaryPrefix_removeNth_after line 30
  3. lemma OAI.BoundedHochschild.KadisonRingrose.unitaryPrefix_tail line 44
  4. lemma OAI.BoundedHochschild.KadisonRingrose.unitaryPrefix_init line 49