OAI/Analysis/Pureness/States/FiniteRegularizationProjections.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CuntzPureness.positive_projection_cut line 12
2. lemma OAI.CuntzPureness.finiteProjection_cut_class line 24
3. theorem OAI.CuntzPureness.regularizedFiniteDimension_projection line 36
4. def OAI.CuntzPureness.regularizedProjectionState line 45