OAI/Analysis/Nuclearity/RepresentedAlgebra.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The actual C*-algebra image of a representation and its surjective range restriction. Nuclearity of this image is a separate mathematical property.

  1. def OAI.WeakPureInfiniteness.representedAlgebra line 14
  2. instance OAI.WeakPureInfiniteness.representedAlgebra_closed line 16
  3. instance OAI.WeakPureInfiniteness.representedAlgebra_cstar line 20
  4. def OAI.WeakPureInfiniteness.representedQuotientMap line 23
  5. theorem OAI.WeakPureInfiniteness.representedQuotientMap_surjective line 25
  6. def OAI.WeakPureInfiniteness.representedInclusion line 30
  7. theorem OAI.WeakPureInfiniteness.representedInclusion_injective line 33
  8. theorem OAI.WeakPureInfiniteness.representedInclusion_apply line 36
  9. theorem OAI.WeakPureInfiniteness.representedInclusion_quotientMap line 39