OAI/Analysis/Pureness/States/FiniteRegularizationAddition.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CuntzPureness.positiveProduct_cut line 10
  2. lemma OAI.CuntzPureness.finitePositiveClass_cut_add line 18
  3. theorem OAI.CuntzPureness.finiteRegularizedValue_add line 23
  4. lemma OAI.CuntzPureness.finiteClass_has_representative line 44
  5. def OAI.CuntzPureness.finiteClassRepresentative line 49
  6. lemma OAI.CuntzPureness.finiteClassRepresentative_spec line 52
  7. def OAI.CuntzPureness.finiteRegularizedFunction line 56
  8. theorem OAI.CuntzPureness.finiteRegularizedFunction_eval line 60
  9. lemma OAI.CuntzPureness.finiteRegularizedFunction_monotone line 67
  10. lemma OAI.CuntzPureness.finiteRegularizedFunction_add line 72
  11. def OAI.CuntzPureness.regularizedFiniteDimension line 83
  12. theorem OAI.CuntzPureness.regularizedFiniteDimension_monotone line 91