OAI/Analysis/Pureness/Completion/CompletedIncrementApproximation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.shrinkPositive line 10
2. lemma OAI.CuntzPureness.shrinkPositive_nonneg line 12
3. lemma OAI.CuntzPureness.shrinkPositive_norm_le line 17
4. lemma OAI.CuntzPureness.shrinkPositive_rank line 25
5. lemma OAI.CuntzPureness.exists_small_matrix_same_rank line 29
6. theorem OAI.CuntzPureness.exists_completed_increment_approximants line 37