OAI/Analysis/Commutator/BicommutantOrbit.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.orbitSubmodule line 20
2. def OAI.Kadison.cyclicSubspace line 30
3. instance OAI.Kadison.(instance at line 33) line 33
4. lemma OAI.Kadison.mem_cyclicSubspace_self line 36
5. lemma OAI.Kadison.cyclicSubspace_invariant line 40
6. lemma OAI.Kadison.projection_commutes_of_invariant line 50
7. lemma OAI.Kadison.cyclic_projection_mem_commutant line 62
8. theorem OAI.Kadison.bicommutant_mem_cyclicSubspace line 68