OAI/Analysis/Nuclearity/PureStateRepresentation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A faithful sum of pure GNS representations. This supplies the faithful representation needed to detect nonzero ideals by product pure states.

  1. structure OAI.WeakPureInfiniteness.PureStateData line 18
  2. def OAI.WeakPureInfiniteness.pureGNSHilbert line 26
  3. def OAI.WeakPureInfiniteness.pureGNSRepresentation line 29
  4. theorem OAI.WeakPureInfiniteness.pureGNSRepresentation_injective line 32
  5. theorem OAI.WeakPureInfiniteness.pureGNSRepresentation_single line 45
  6. theorem OAI.WeakPureInfiniteness.pureGNS_operator_eq_zero line 58