OAI/Analysis/Pureness/Comparison/Comparison.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzComparison.CuntzSubequiv line 11
2. theorem OAI.CuntzComparison.cuntzSubequiv_iff_sequence line 14
3. theorem OAI.CuntzComparison.cuntzSubequiv_iff_norm line 25
4. theorem OAI.CuntzComparison.cuntzSubequiv_of_exact line 31
5. theorem OAI.CuntzComparison.zero_cuntzSubequiv line 35
6. theorem OAI.CuntzComparison.cuntzSubequiv_zero_iff line 38
7. theorem OAI.CuntzComparison.CuntzSubequiv.of_tendsto line 41
8. theorem OAI.CuntzComparison.CuntzSubequiv.compress line 46
9. theorem OAI.CuntzComparison.CuntzSubequiv.trans line 54