OAI/Analysis/BoundedHochschild/FixedFactorizationLimits.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Pointwise weak operator limits retain a fixed representation and left factor, while the bounded right factor is allowed to vary.

  1. def OAI.BoundedHochschild.KadisonRingrose.weakFactorFamily line 18
  2. lemma OAI.BoundedHochschild.KadisonRingrose.weakFactorFamily_continuous line 22
  3. theorem OAI.BoundedHochschild.KadisonRingrose.fixedFactorization_isClosed line 28
  4. theorem OAI.BoundedHochschild.KadisonRingrose.factorization_of_pointwise_weak_limit line 48