OAI/Analysis/Commutator/SeparableReducingHull.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.SeparableReducingHull.generator line 20
2. def OAI.Kadison.SeparableReducingHull.orbit line 23
3. def OAI.Kadison.SeparableReducingHull.hull line 26
4. lemma OAI.Kadison.SeparableReducingHull.hull_closed line 29
5. instance OAI.Kadison.SeparableReducingHull.hull_complete line 32
6. lemma OAI.Kadison.SeparableReducingHull.vector_mem line 35
7. lemma OAI.Kadison.SeparableReducingHull.generator_invariant line 40
8. lemma OAI.Kadison.SeparableReducingHull.invariant line 53
9. lemma OAI.Kadison.SeparableReducingHull.star_invariant line 57
10. instance OAI.Kadison.SeparableReducingHull.hull_separable line 61
11. def OAI.Kadison.SeparableReducingHull.reducingAlgebra line 66
12. lemma OAI.Kadison.SeparableReducingHull.reducingAlgebra_closed line 88
13. lemma OAI.Kadison.SeparableReducingHull.generator_mem_reducingAlgebra line 98
14. lemma OAI.Kadison.SeparableReducingHull.generated_reduces line 101