OAI/Analysis/KadisonKastler/LocalCoefficientTests.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Original-space coefficients from a reducing corner

Strong density of the restricted algebra gives finite coefficient approximants in the original algebra. This step needs neither faithful restriction nor norm bounds on the chosen coefficient approximants.

  1. theorem OAI.KadisonKastler.exists_strong_coefficient_approx line 21
  2. theorem OAI.KadisonKastler.exists_original_coefficient_approx line 53