OAI/Analysis/Nuclearity/PositiveSpanningSequence.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Continuous linear identities and commutation extend from a dense sequence in the positive cone, which linearly spans a C*-algebra.

  1. lemma OAI.WeakPureInfiniteness.exists_dense_positive_sequence line 16
  2. lemma OAI.WeakPureInfiniteness.continuousLinearMap_ext_positive_sequence line 21
  3. lemma OAI.WeakPureInfiniteness.commute_of_positive_sequence line 32
  4. lemma OAI.WeakPureInfiniteness.abelian_range_of_positive_sequence line 40