OAI/Analysis/Nuclearity/NuclearConeNullspace.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The tensor-functional cone in KR02 Lemma 7.18. The nullspace argument uses the elementary-span property of its closed tensor ideal (Blackadar 3.3 / Tomiyama 5).

  1. def OAI.WeakPureInfiniteness.abelianCompressionIndex line 26
  2. def OAI.WeakPureInfiniteness.abelianTensorCone line 29
  3. theorem OAI.WeakPureInfiniteness.inclusionTensorFunctional_mem_cone_of_elementary_span line 36