OAI/Analysis/BoundedHochschild/FiniteColumnCorners.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Finite initial sections of a countable matrix system form full matrix systems in their actual (possibly proper) corners.

  1. def OAI.BoundedHochschild.KadisonRingrose.finiteColumnProjection line 20
  2. lemma OAI.BoundedHochschild.KadisonRingrose.finiteColumnProjection_isProjection line 24
  3. lemma OAI.BoundedHochschild.KadisonRingrose.finiteColumnProjection_mul_column line 30
  4. lemma OAI.BoundedHochschild.KadisonRingrose.column_star_mul_finiteColumnProjection line 38
  5. def OAI.BoundedHochschild.KadisonRingrose.finiteColumnMatrixSystem line 43
  6. lemma OAI.BoundedHochschild.KadisonRingrose.finiteColumnMatrixSystem_entry line 65