OAI/Analysis/Commutator/NormalPredual.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.NormalPredual.coefficient line 24
2. def OAI.Kadison.NormalPredual.finiteTests line 28
3. lemma OAI.Kadison.NormalPredual.finiteTests_separable line 31
4. theorem OAI.Kadison.NormalPredual.mem_closure_of_strong_null line 38
5. def OAI.Kadison.NormalPredual.BoundedWOTContinuous line 64
6. lemma OAI.Kadison.NormalPredual.coefficient_normal line 68
7. theorem OAI.Kadison.NormalPredual.normal_of_mem_closure line 78