OAI/Analysis/KadisonKastler/MinimalFamilyModule.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Every member of a minimal row family in a fixed completely bounded orbit closure is right modular. The auxiliary factorization is constructed before applying the central-support localization argument.

  1. theorem OAI.KadisonKastler.minimal_row_family_right_module_of_factorization line 21
  2. theorem OAI.KadisonKastler.minimal_row_family_right_module line 51