OAI/Analysis/Commutator/WeakConvergence.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.WeakOperatorLimit.Converges line 22
2. lemma OAI.Kadison.WeakOperatorLimit.Converges.add line 25
3. lemma OAI.Kadison.WeakOperatorLimit.Converges.sub line 30
4. lemma OAI.Kadison.WeakOperatorLimit.converges_const line 35
5. lemma OAI.Kadison.WeakOperatorLimit.Converges.mul_right line 37
6. lemma OAI.Kadison.WeakOperatorLimit.Converges.mul_left line 42
7. lemma OAI.Kadison.WeakOperatorLimit.Converges.commutator line 47
8. lemma OAI.Kadison.WeakOperatorLimit.Converges.unique line 51
9. lemma OAI.Kadison.WeakOperatorLimit.Converges.eq_const line 56
10. lemma OAI.Kadison.WeakOperatorLimit.Converges.norm line 62
11. lemma OAI.Kadison.WeakOperatorLimit.Converges.commutes line 65
12. lemma OAI.Kadison.WeakOperatorLimit.Converges.commutator_norm line 70
13. lemma OAI.Kadison.WeakOperatorLimit.Converges.preserves_sandwich line 74
14. lemma OAI.Kadison.WeakOperatorLimit.Converges.dist line 78