OAI/Analysis/Pureness/Operators/SelfCommutatorSeparation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.selfCommutatorDownCone line 10
2. lemma OAI.CuntzPureness.selfCommutatorDownCone_zero line 14
3. lemma OAI.CuntzPureness.selfCommutatorDownCone_smul line 17
4. lemma OAI.CuntzPureness.selfCommutatorDownCone_convex line 23
5. theorem OAI.CuntzPureness.tracialState_of_one_not_mem_closure line 29
6. theorem OAI.CuntzPureness.exists_selfCommutatorSpace_ge_half line 60