OAI/Analysis/BoundedHochschild/CentralSupportCuts.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Central cuts of projection supports.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.IsCentralSupport.eq_zero_iff line 18
  2. lemma OAI.BoundedHochschild.KadisonRingrose.IsCentralSupport.centralCut line 27
  3. lemma OAI.BoundedHochschild.KadisonRingrose.IsCentralSupport.centralCut_one line 44
  4. lemma OAI.BoundedHochschild.KadisonRingrose.IsCentralSupport.central_cut_nonzero line 49