OAI/Analysis/Pureness/Operators/FiniteDimensionRegularization.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.finiteRegularizedValue line 11
2. lemma OAI.CuntzPureness.finiteRegularizedValue_inclusion line 15
3. lemma OAI.CuntzPureness.finiteRegularizedValue_mono_same line 20
4. theorem OAI.CuntzPureness.finiteRegularizedValue_mono line 33
5. lemma OAI.CuntzPureness.finiteRegularizedValue_le line 46
6. lemma OAI.CuntzPureness.cut_class_value_le_regularized line 57
7. lemma OAI.CuntzPureness.finiteRegularizedValue_zero line 62
8. lemma OAI.CuntzPureness.finiteCutValue_antitone line 70