OAI/Analysis/FactorGeneration/Generation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Relative generation under represented-factor hypotheses: unitaries in a dense G-delta set satisfy W*(N,u)=M.

  1. theorem OAI.Generator.Tracial.relative_generation_at_continuity line 31
  2. theorem OAI.Generator.Tracial.represented_relative_generation line 89
  3. theorem OAI.Generator.Tracial.represented_four_selfAdjoint_generators line 106
  4. theorem OAI.Generator.Tracial.represented_two_selfAdjoint_generators line 159
  5. theorem OAI.Generator.Tracial.represented_single_generator line 186
  6. theorem OAI.Generator.Tracial.singlyGenerated_of_tracialRepresentation line 196