OAI/Analysis/OperatorAlgebra/CyclicStandardIntertwiner.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The application-specific standard representation and bounded intertwiner for a tested vector of a representation of a separable C*-algebra.

  1. theorem OAI.WeakPureInfiniteness.exists_cyclic_standard_intertwiner line 19