VonNeumannSpectralCut.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Positive spectral cuts in a von Neumann algebra

The support of the positive part of x* x - t gives the required projection. The existing concrete range-projection construction supplies its membership in the von Neumann algebra.

theorem OAI.KadisonKastler.publishedVonNeumannSpectralCut line 35
Source documentation
Positive support and continuous functional calculus give spectral cuts.
```
theorem publishedVonNeumannSpectralCut : PublishedVonNeumannSpectralCut.{u} := by
…
```