OAI/Analysis/JiangSu/CuntzSemigroup/FiniteDimensionRegularization.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Pureness.finiteRegularizedValue line 15
  2. lemma OAI.Pureness.finiteRegularizedValue_inclusion line 19
  3. lemma OAI.Pureness.finiteRegularizedValue_mono_same line 24
  4. theorem OAI.Pureness.finiteRegularizedValue_mono line 37
  5. lemma OAI.Pureness.finiteRegularizedValue_le line 50
  6. lemma OAI.Pureness.cut_class_value_le_regularized line 61
  7. lemma OAI.Pureness.finiteRegularizedValue_zero line 66
  8. lemma OAI.Pureness.finiteCutValue_antitone line 74
  9. lemma OAI.Pureness.positiveProduct_cut line 83
  10. lemma OAI.Pureness.finitePositiveClass_cut_add line 91
  11. theorem OAI.Pureness.finiteRegularizedValue_add line 96
  12. lemma OAI.Pureness.finiteClass_has_representative line 117
  13. def OAI.Pureness.finiteClassRepresentative line 122
  14. lemma OAI.Pureness.finiteClassRepresentative_spec line 125
  15. def OAI.Pureness.finiteRegularizedFunction line 129
  16. theorem OAI.Pureness.finiteRegularizedFunction_eval line 133
  17. lemma OAI.Pureness.finiteRegularizedFunction_monotone line 140
  18. lemma OAI.Pureness.finiteRegularizedFunction_add line 145
  19. def OAI.Pureness.regularizedFiniteDimension line 156
  20. theorem OAI.Pureness.regularizedFiniteDimension_monotone line 164
  21. theorem OAI.Pureness.finiteRegularizedValue_lowerSemicontinuous line 167
  22. theorem OAI.Pureness.regularizedFiniteDimension_eval line 186
  23. theorem OAI.Pureness.regularizedFiniteDimension_le line 192
  24. lemma OAI.Pureness.cut_value_le_twice_regularized line 199
  25. theorem OAI.Pureness.regularizedFiniteDimension_idempotent line 211
  26. theorem OAI.Pureness.regularizedFiniteDimension_eq_of_lowerSemicontinuous line 221