OAI/Analysis/Pureness/Completion/CompletedUniformComparison.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CuntzPureness.continuous_matrixTrace_eval line 11
2. lemma OAI.CuntzPureness.continuous_completedTraceValue_eval line 16
3. theorem OAI.CuntzPureness.lowerSemicontinuous_completedRootRank line 20
4. lemma OAI.CuntzPureness.isOpen_lt_completedRootRank line 29
5. theorem OAI.CuntzPureness.uniform_completedCompression_index line 38
6. lemma OAI.CuntzPureness.completedCompression_eventually_ne_zero line 51
7. theorem OAI.CuntzPureness.exists_nonzero_completedCompression_rank_gap line 62