OAI/Analysis/KadisonKastler/CenteredTestShiftLimits.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The centered test is preserved by the remote graph shifts

  1. theorem OAI.KadisonKastler.ModularConjugationData.centeredTest_decomposition line 22
  2. theorem OAI.KadisonKastler.ModularConjugationData.coisometry_centeredTest_tendsto line 35
  3. theorem OAI.KadisonKastler.ModularConjugationData.isometry_centeredTest_tendsto line 47