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"
```