OAI/Analysis/Nuclearity/NuclearRepresentedQuotient.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Application of the proved quotient tensor bound to the exact represented unitization input in Corollary 1.3 (Choi--Effros, Corollary 3.3).

  1. lemma OAI.WeakPureInfiniteness.representedQuotient_separable line 19
  2. theorem OAI.WeakPureInfiniteness.nuclear_represented_quotient_tensorNorm line 24
  3. lemma OAI.WeakPureInfiniteness.unitization_separable line 38
  4. theorem OAI.WeakPureInfiniteness.nuclear_unitizedFactorImageNuclear line 42