OAI/Analysis/Pureness/Projections/ProjectionDimension.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.CuntzPureness.ProjectionDimension line 8
2. instance OAI.CuntzPureness.projectionDimensionCoeFun line 17
3. lemma OAI.CuntzPureness.ProjectionDimension.sub line 21
4. lemma OAI.CuntzPureness.ProjectionDimension.mono line 29
5. lemma OAI.CuntzPureness.ProjectionDimension.le_one line 35
6. lemma OAI.CuntzPureness.ProjectionDimension.one_sub line 39