OAI/Analysis/Pureness/Comparison/UniformTwoNorm.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CuntzComparison.uniformTwoNorm line 11
  2. lemma OAI.CuntzComparison.twoNorm_range_bddAbove line 15
  3. theorem OAI.CuntzComparison.twoNorm_le_uniform line 22
  4. theorem OAI.CuntzComparison.uniformTwoNorm_nonneg line 25
  5. theorem OAI.CuntzComparison.uniformTwoNorm_le_norm line 29
  6. theorem OAI.CuntzComparison.uniformTwoNorm_zero line 34
  7. theorem OAI.CuntzComparison.uniformTwoNorm_one line 38
  8. theorem OAI.CuntzComparison.uniformTwoNorm_add_le line 41
  9. theorem OAI.CuntzComparison.uniformTwoNorm_star line 49
  10. theorem OAI.CuntzComparison.uniformTwoNorm_neg line 54
  11. theorem OAI.CuntzComparison.uniformTwoNorm_smul_le line 60
  12. theorem OAI.CuntzComparison.uniformTwoNorm_mul_left line 67
  13. theorem OAI.CuntzComparison.uniformTwoNorm_mul_right line 74
  14. theorem OAI.CuntzComparison.uniformTwoNorm_sub_le line 79
  15. theorem OAI.CuntzComparison.uniformTwoNorm_lipschitz line 88
  16. theorem OAI.CuntzComparison.continuous_uniformTwoNorm line 94