OAI/Analysis/Nuclearity/PureProductRepresentation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The product of the faithful pure-GNS sums and its total cyclic vectors.

  1. abbrev OAI.WeakPureInfiniteness.pureProductRepresentation line 22
  2. theorem OAI.WeakPureInfiniteness.pureProductEvaluation_isometry line 28
  3. theorem OAI.WeakPureInfiniteness.gns_unital_apply line 33
  4. def OAI.WeakPureInfiniteness.pureCyclicVector line 36
  5. theorem OAI.WeakPureInfiniteness.pureGNS_inner_single line 39
  6. theorem OAI.WeakPureInfiniteness.norm_pureCyclicVector line 45
  7. theorem OAI.WeakPureInfiniteness.pureProduct_cyclic_total line 50