OAI/Analysis/KadisonSimilarity/Tracial/TracialInclusionNormality.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A trace-preserving inclusion with closed source trace-vector balls has normal range in a faithful concrete finite trace representation.

  1. theorem OAI.KadisonSimilarity.tracePreservingVector_inner line 26
  2. theorem OAI.KadisonSimilarity.tracePreservingVector_norm line 30
  3. def OAI.KadisonSimilarity.tracialInclusionIsometry line 36
  4. theorem OAI.KadisonSimilarity.tracialInclusionIsometry_vector line 40
  5. theorem OAI.KadisonSimilarity.tracialInclusion_trace_balls_closed line 45
  6. theorem OAI.KadisonSimilarity.tracialInclusion_normal_range line 59
  7. theorem OAI.KadisonSimilarity.tracialInclusion_normal_range_of_predual line 100