OAI/Analysis/Pureness/Cuntz/FiniteCuntzSums.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.finiteSumColumn line 10
2. lemma OAI.CuntzPureness.matrixInterleaveRaw_entry' line 14
3. lemma OAI.CuntzPureness.finiteSumColumn_sandwich line 19
4. theorem OAI.CuntzPureness.finitePositiveClass_sum_le line 28
5. theorem OAI.CuntzPureness.finitePositiveClass_sum_bound line 48