OAI/Analysis/KadisonSimilarity/Tracial/PredualGNSSeparable.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A normal positive functional on an algebra with separable predual has a separable GNS space. Countably many dual evaluations give a total family of GNS vectors.

  1. theorem OAI.KadisonSimilarity.exists_countable_total_gns_vectors line 23
  2. theorem OAI.KadisonSimilarity.gns_separable_of_predual line 40