OAI/Analysis/WeakInfiniteness/ElementaryComparison.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakPureInfiniteness.zero_cuntzSubequiv line 31
2. lemma OAI.WeakPureInfiniteness.CuntzSubequiv.of_exact line 37
3. lemma OAI.WeakPureInfiniteness.continuous_matrix_mul line 44
4. lemma OAI.WeakPureInfiniteness.continuous_matrix_sandwich line 58
5. lemma OAI.WeakPureInfiniteness.matrix_mul_assoc line 64
6. lemma OAI.WeakPureInfiniteness.matrix_conjTranspose_mul line 69
7. lemma OAI.WeakPureInfiniteness.cuntzSubequiv_iff_mem_closure line 74
8. lemma OAI.WeakPureInfiniteness.CuntzSubequiv.of_tendsto line 86
9. lemma OAI.WeakPureInfiniteness.CuntzSubequiv.trans line 94
10. lemma OAI.WeakPureInfiniteness.cuntzSubequiv_refl line 114