src/HOL/NthRoot.thy
changeset 51478 270b21f3ae0a
parent 49962 a8cc904a6820
child 51483 dc39d69774bb
     1.1 --- a/src/HOL/NthRoot.thy	Fri Mar 22 10:41:43 2013 +0100
     1.2 +++ b/src/HOL/NthRoot.thy	Fri Mar 22 10:41:43 2013 +0100
     1.3 @@ -338,6 +338,18 @@
     1.4  apply (simp_all add: isCont_root_pos isCont_root_neg isCont_root_zero)
     1.5  done
     1.6  
     1.7 +lemma tendsto_real_root[tendsto_intros]:
     1.8 +  "(f ---> x) F \<Longrightarrow> 0 < n \<Longrightarrow> ((\<lambda>x. root n (f x)) ---> root n x) F"
     1.9 +  using isCont_tendsto_compose[OF isCont_real_root, of n f x F] .
    1.10 +
    1.11 +lemma continuous_real_root[continuous_intros]:
    1.12 +  "continuous F f \<Longrightarrow> 0 < n \<Longrightarrow> continuous F (\<lambda>x. root n (f x))"
    1.13 +  unfolding continuous_def by (rule tendsto_real_root)
    1.14 +  
    1.15 +lemma continuous_on_real_root[continuous_on_intros]:
    1.16 +  "continuous_on s f \<Longrightarrow> 0 < n \<Longrightarrow> continuous_on s (\<lambda>x. root n (f x))"
    1.17 +  unfolding continuous_on_def by (auto intro: tendsto_real_root)
    1.18 +
    1.19  lemma DERIV_real_root:
    1.20    assumes n: "0 < n"
    1.21    assumes x: "0 < x"
    1.22 @@ -491,6 +503,18 @@
    1.23  lemma isCont_real_sqrt: "isCont sqrt x"
    1.24  unfolding sqrt_def by (rule isCont_real_root [OF pos2])
    1.25  
    1.26 +lemma tendsto_real_sqrt[tendsto_intros]:
    1.27 +  "(f ---> x) F \<Longrightarrow> ((\<lambda>x. sqrt (f x)) ---> sqrt x) F"
    1.28 +  unfolding sqrt_def by (rule tendsto_real_root [OF _ pos2])
    1.29 +
    1.30 +lemma continuous_real_sqrt[continuous_intros]:
    1.31 +  "continuous F f \<Longrightarrow> continuous F (\<lambda>x. sqrt (f x))"
    1.32 +  unfolding sqrt_def by (rule continuous_real_root [OF _ pos2])
    1.33 +  
    1.34 +lemma continuous_on_real_sqrt[continuous_on_intros]:
    1.35 +  "continuous_on s f \<Longrightarrow> 0 < n \<Longrightarrow> continuous_on s (\<lambda>x. sqrt (f x))"
    1.36 +  unfolding sqrt_def by (rule continuous_on_real_root [OF _ pos2])
    1.37 +
    1.38  lemma DERIV_real_sqrt_generic:
    1.39    assumes "x \<noteq> 0"
    1.40    assumes "x > 0 \<Longrightarrow> D = inverse (sqrt x) / 2"