OAI/Analysis/WeakInfiniteness/CuntzCopies.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WeakPureInfiniteness.continuous_blockSum line 30
  2. lemma OAI.WeakPureInfiniteness.CuntzSubequiv.blockSum line 34
  3. def OAI.WeakPureInfiniteness.matrixSubmatrix line 59
  4. lemma OAI.WeakPureInfiniteness.continuous_matrixSubmatrix line 63
  5. lemma OAI.WeakPureInfiniteness.CuntzSubequiv.submatrix_left line 67
  6. lemma OAI.WeakPureInfiniteness.CuntzSubequiv.reindex_right line 81
  7. lemma OAI.WeakPureInfiniteness.diagonalCopies_submatrix line 91
  8. lemma OAI.WeakPureInfiniteness.diagonalCopies_cuntzSubequiv line 97
  9. lemma OAI.WeakPureInfiniteness.diagonalCopies_double line 103
  10. lemma OAI.WeakPureInfiniteness.ProperlyInfinite.diagonal_powers line 118
  11. lemma OAI.WeakPureInfiniteness.ProperlyInfinite.diagonal_absorbs line 131