OAI/Analysis/Pureness/Operators/DenseKernelClosedIdeal.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.denseKernelImage line 12
2. lemma OAI.CuntzPureness.denseKernelImage_mem line 14
3. lemma OAI.CuntzPureness.denseKernelImage_mul_left line 17
4. lemma OAI.CuntzPureness.denseKernelImage_mul_right line 23
5. lemma OAI.CuntzPureness.denseKernelImage_star line 29
6. lemma OAI.CuntzPureness.denseKernelClosure_mul_left line 38
7. lemma OAI.CuntzPureness.denseKernelClosure_mul_right line 50
8. def OAI.CuntzPureness.denseKernelClosedIdeal line 61
9. lemma OAI.CuntzPureness.denseKernelClosedIdeal_coe line 79
10. lemma OAI.CuntzPureness.denseKernelClosedIdeal_mem line 85
11. lemma OAI.CuntzPureness.denseKernelClosedIdeal_map_zero line 94