OAI/Analysis/KadisonKastler/SimultaneousModularCluster.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Coordinate images of a minimal simultaneous row family are minimal. The proved one-map theorem therefore produces a common modular cluster.

  1. theorem OAI.KadisonKastler.family_orbitClosure_coordinate line 15
  2. theorem OAI.KadisonKastler.minimal_family_coordinate line 25
  3. theorem OAI.KadisonKastler.exists_simultaneous_modular_cluster line 57