WeakMapCompact.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The completely bounded ball is compact in the pointwise weak operator topology.

structure OAI.KadisonKastler.BoundedWeakAlgebraMap line 22
def OAI.KadisonKastler.boundedWeakAlgebraCoefficients line 26
instance OAI.KadisonKastler.boundedWeakAlgebraMapTopology line 30
theorem OAI.KadisonKastler.isCompact_boundedWeakAlgebraMap line 35
Source documentation
All matrix bounds are retained at a pointwise weak cluster point.
```
theorem isCompact_boundedWeakAlgebraMap (M : VonNeumannAlgebra H) {c : ℝ} (hc : 0 ≤ c) :
    IsCompact (Set.univ : Set (BoundedWeakAlgebraMap M c)) := by
…
```
Mentions: OAI.KadisonKastler.BoundedWeakAlgebraMap