OAI/Analysis/KadisonSimilarity/Tracial/UltrapowerNormality.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual tracial ultrapower has closed bounded trace-vector balls, hence its faithful GNS representation is a von Neumann algebra.

  1. theorem OAI.KadisonSimilarity.ultrapower_trace_balls_closed line 19
  2. theorem OAI.KadisonSimilarity.ultrapower_gns_normal_range line 59