OAI/Analysis/BoundedHochschild/NormalGNSConvergence.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

On bounded nets the given predual topology agrees with weak operator convergence in the faithful normal representation.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.normalGNS_predual_tendsto line 21
  2. lemma OAI.BoundedHochschild.KadisonRingrose.predual_tendsto_of_normalGNS line 31