OAI/Analysis/IrrationalRotation/Operators/BicommutantStrongTopology.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Invariant233.BicommutantDensity.strongView line 13
2. theorem OAI.Invariant233.BicommutantDensity.strongView_apply line 16
3. theorem OAI.Invariant233.BicommutantDensity.underlying_apply line 17
4. theorem OAI.Invariant233.BicommutantDensity.underlying_strongView line 20
5. theorem OAI.Invariant233.BicommutantDensity.strongView_underlying line 22
6. theorem OAI.Invariant233.BicommutantDensity.mem_strongClosure_iff line 25
7. theorem OAI.Invariant233.BicommutantDensity.isClosed_strongCentralizer line 48
8. theorem OAI.Invariant233.BicommutantDensity.strongClosure_subset_bicommutant line 52