OAI/Analysis/Pureness/Divisibility/Hereditary.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.sandwichSubalgebra line 10
2. def OAI.CuntzPureness.hereditarySubalgebra line 26
3. def OAI.CuntzPureness.hereditaryCarrier line 29
4. lemma OAI.CuntzPureness.hereditarySubalgebra_coe line 31
5. instance OAI.CuntzPureness.hereditarySubalgebra_closed line 34
6. lemma OAI.CuntzPureness.hereditary_sqrt_mem line 37
7. lemma OAI.CuntzPureness.self_mem_hereditary line 43
8. lemma OAI.CuntzPureness.hereditary_sandwich_mem line 49
9. lemma OAI.CuntzPureness.sqrt_sandwich_mem_hereditary line 62
10. lemma OAI.CuntzPureness.normalizedRoot_mem_hereditary line 67