src/HOL/NthRoot.thy
changeset 60615 e5fa1d5d3952
parent 60141 833adf7db7d8
child 60758 d8d85a8172b5
     1.1 --- a/src/HOL/NthRoot.thy	Mon Jun 29 13:49:21 2015 +0200
     1.2 +++ b/src/HOL/NthRoot.thy	Tue Jun 30 13:56:16 2015 +0100
     1.3 @@ -448,6 +448,11 @@
     1.4  lemmas real_sqrt_le_1_iff [simp] = real_sqrt_le_iff [where y=1, unfolded real_sqrt_one]
     1.5  lemmas real_sqrt_eq_1_iff [simp] = real_sqrt_eq_iff [where y=1, unfolded real_sqrt_one]
     1.6  
     1.7 +lemma sqrt_add_le_add_sqrt:
     1.8 +  assumes "0 \<le> x" "0 \<le> y"
     1.9 +  shows "sqrt (x + y) \<le> sqrt x + sqrt y"
    1.10 +by (rule power2_le_imp_le) (simp_all add: power2_sum assms)
    1.11 +
    1.12  lemma isCont_real_sqrt: "isCont sqrt x"
    1.13  unfolding sqrt_def by (rule isCont_real_root)
    1.14