OAI/Analysis/KadisonKastler/SimultaneousRowUltralimit.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A single ultrafilter of normalized rows realizes the simultaneous modular cluster. Every completely bounded map can be included as a coordinate.

  1. theorem OAI.KadisonKastler.exists_simultaneous_modular_rows line 24
  2. structure OAI.KadisonKastler.BoundedMapDatum line 65
  3. abbrev OAI.KadisonKastler.UniversalMapFamily line 71
  4. theorem OAI.KadisonKastler.exists_universal_modular_rows line 74