OAI/Analysis/WeakInfiniteness/FiniteComparison.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakPureInfiniteness.fiberDiagonal line 30
2. lemma OAI.WeakPureInfiniteness.continuous_fiberDiagonal line 34
3. lemma OAI.WeakPureInfiniteness.copies_cuntz_fiberDiagonal line 38
4. lemma OAI.WeakPureInfiniteness.orthogonal_fiberDiagonal_cuntz_sum line 58
5. lemma OAI.WeakPureInfiniteness.copies_cuntz_of_common_orthogonal line 85