CountableCyclicDecomposition.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

An orthogonal cyclic decomposition is countable on a separable Hilbert space, as required for the normal standard-representation reduction.

theorem OAI.KadisonSimilarity.CyclicDecompositionData.generators_countable line 20
Source documentation
Normalized nonzero cyclic generators have disjoint open half-balls, so separability makes the family countable.
```
theorem generators_countable (D : CyclicDecompositionData N) : Countable D.generators := by
…
```
Mentions: OAI.KadisonSimilarity.CyclicDecompositionData