OAI/Analysis/OperatorAlgebra/GNSBundledIntertwining.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Intertwining from vector formulas, stated entirely in the bundled GNS space.

  1. lemma OAI.WeakPureInfiniteness.gnsBundledLeft_intertwines line 13
  2. lemma OAI.WeakPureInfiniteness.gnsBundledRight_intertwines line 20