OAI/Analysis/KadisonKastler/RectangularWeakCompact.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Weak operator compactness for the rectangular operators in a fixed factorization. The source and target Hilbert spaces may differ.

  1. theorem OAI.KadisonKastler.exists_weak_rectangular_operator_ultralimit line 19
  2. def OAI.KadisonKastler.weakRectangularBall line 40
  3. theorem OAI.KadisonKastler.isCompact_weakRectangularBall line 45