OAI/Analysis/PureInfiniteness/FunctionalTensorRepresentation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous GNS data, with its commutant kept as an abstract C*-algebra. This interface does not add a hypothesis: every finite real functional family has such a representation by functionalTensorRepresentation_nonempty.

  1. structure OAI.WeakPureInfiniteness.FunctionalTensorRepresentation line 16
  2. theorem OAI.WeakPureInfiniteness.functionalTensorRepresentation_nonempty line 40