OAI/Analysis/Nuclearity/CommutantTensorWitness.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A finite separating family is a single self-adjoint tensor test. The representing data are constructed from the actual unitized GNS commutant.

  1. def OAI.WeakPureInfiniteness.FunctionalTensorRepresentation.original line 25
  2. lemma OAI.WeakPureInfiniteness.FunctionalTensorRepresentation.original_commute line 29
  3. def OAI.WeakPureInfiniteness.FunctionalTensorRepresentation.tensorElement line 32
  4. lemma OAI.WeakPureInfiniteness.FunctionalTensorRepresentation.tensorElement_selfAdjoint line 36
  5. def OAI.WeakPureInfiniteness.FunctionalTensorRepresentation.tensorFunctional line 46
  6. lemma OAI.WeakPureInfiniteness.FunctionalTensorRepresentation.tensorFunctional_element line 50