OAI/Analysis/CStarAlgebra/PureInfiniteness/Shrinking.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MainGap.conditional_shrinking line 21
  2. theorem OAI.MainGap.shrinking_unital_local line 86
  3. def OAI.MainGap.matrixMap line 102
  4. lemma OAI.MainGap.matrixMap_mul line 105
  5. lemma OAI.MainGap.matrixMap_star line 112
  6. lemma OAI.MainGap.continuous_matrixMap line 119
  7. lemma OAI.MainGap.FiniteCuntzLE.map line 127
  8. lemma OAI.MainGap.ProperlyInfinite.map line 136
  9. lemma OAI.MainGap.unitization_Her line 158
  10. lemma OAI.MainGap.unitization_inr_snd_of_Her line 175
  11. lemma OAI.MainGap.unitization_proper_hereditary line 180
  12. def OAI.MainGap.NormSignal line 201
  13. theorem OAI.MainGap.shrinking_nonunital line 205