OAI/Analysis/Commutator/FactorCorner.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.FactorCorner.supportSpace line 19
2. instance OAI.Kadison.FactorCorner.(instance at line 22) line 22
3. lemma OAI.Kadison.FactorCorner.generator_mem line 25
4. lemma OAI.Kadison.FactorCorner.supportSpace_invariant line 29
5. lemma OAI.Kadison.FactorCorner.invariant_of_mem line 38
6. lemma OAI.Kadison.FactorCorner.invariant_of_commutant line 45
7. lemma OAI.Kadison.FactorCorner.projection_commutant line 57
8. lemma OAI.Kadison.FactorCorner.projection_mem line 63
9. def OAI.Kadison.FactorCorner.IsFactor line 74
10. lemma OAI.Kadison.FactorCorner.centralSupport_eq_one line 77
11. theorem OAI.Kadison.FactorCorner.exists_nonzero_corner line 95
12. theorem OAI.Kadison.FactorCorner.exists_linking_partialIsometry line 114