OAI/Analysis/Pureness/Cuntz/CuntzRescaling.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CuntzPureness.CuntzSubequiv.smul_left line 10
2. theorem OAI.CuntzPureness.positive_smul_cuntz_equiv line 21
3. theorem OAI.CuntzPureness.exists_small_cuntz_equivalent line 28
4. theorem OAI.CuntzPureness.exists_summable_cuntz_rescaling line 39