equal
deleted
inserted
replaced
444 lemma sqrt_add_le_add_sqrt: |
444 lemma sqrt_add_le_add_sqrt: |
445 assumes x: "0 \<le> x" and y: "0 \<le> y" |
445 assumes x: "0 \<le> x" and y: "0 \<le> y" |
446 shows "sqrt (x + y) \<le> sqrt x + sqrt y" |
446 shows "sqrt (x + y) \<le> sqrt x + sqrt y" |
447 apply (rule power2_le_imp_le) |
447 apply (rule power2_le_imp_le) |
448 apply (simp add: power2_sum x y) |
448 apply (simp add: power2_sum x y) |
449 apply (simp add: mult_nonneg_nonneg x y) |
|
450 apply (simp add: x y) |
449 apply (simp add: x y) |
451 done |
450 done |
452 |
451 |
453 lemma bounded_linear_Pair: |
452 lemma bounded_linear_Pair: |
454 assumes f: "bounded_linear f" |
453 assumes f: "bounded_linear f" |