OAI/Analysis/Nuclearity/NuclearCoefficientApproximation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Application of the tensor-ideal step to the actual point-norm cone. The elementary-span property of the GNS common-null ideals (Blackadar 3.3 / Tomiyama 5) supplies coefficient approximation.

  1. theorem OAI.WeakPureInfiniteness.inclusion_mem_coefficientClosure_of_elementary_span line 23
  2. theorem OAI.WeakPureInfiniteness.approximatelyOneStepAlong_of_nuclear_and_elementary_span line 53