SpatialSeparability.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Separability of the completed spatial tensor product

theorem OAI.KadisonKastler.dense_span_tensorVector line 20

Source documentation

A countable dense family in each leg gives a countable total family of pure tensors in the completed Hilbert tensor product.

theorem dense_span_tensorVector {f : ℕ → H} {g : ℕ → K}
    (hf : DenseRange f) (hg : DenseRange g) :
    Dense (Submodule.span ℂ (Set.range (fun p : ℕ × ℕ => tensorVector (g p.2) (f p.1))) :
      Set (SpatialHilbert H K)) := by
…

Mentions: OAI.KadisonKastler.tensorVector

instance OAI.KadisonKastler.spatialHilbert_separable line 43
instance OAI.KadisonKastler.spatialHilbert_nontrivial line 54
Source documentation
A pair of nonzero vectors witnesses nontriviality after completion.
```
instance spatialHilbert_nontrivial [Nontrivial H] [Nontrivial K] :
    Nontrivial (SpatialHilbert H K) := by
…
```