src/HOL/NthRoot.thy
changeset 57155 5c59114ff0cb
parent 56889 48a745e1bde7
child 57275 0ddb5b755cdc
equal deleted inserted replaced
57154:f0eff6393a32 57155:5c59114ff0cb
   459 lemma continuous_real_sqrt[continuous_intros]:
   459 lemma continuous_real_sqrt[continuous_intros]:
   460   "continuous F f \<Longrightarrow> continuous F (\<lambda>x. sqrt (f x))"
   460   "continuous F f \<Longrightarrow> continuous F (\<lambda>x. sqrt (f x))"
   461   unfolding sqrt_def by (rule continuous_real_root)
   461   unfolding sqrt_def by (rule continuous_real_root)
   462   
   462   
   463 lemma continuous_on_real_sqrt[continuous_intros]:
   463 lemma continuous_on_real_sqrt[continuous_intros]:
   464   "continuous_on s f \<Longrightarrow> 0 < n \<Longrightarrow> continuous_on s (\<lambda>x. sqrt (f x))"
   464   "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. sqrt (f x))"
   465   unfolding sqrt_def by (rule continuous_on_real_root)
   465   unfolding sqrt_def by (rule continuous_on_real_root)
   466 
   466 
   467 lemma DERIV_real_sqrt_generic:
   467 lemma DERIV_real_sqrt_generic:
   468   assumes "x \<noteq> 0"
   468   assumes "x \<noteq> 0"
   469   assumes "x > 0 \<Longrightarrow> D = inverse (sqrt x) / 2"
   469   assumes "x > 0 \<Longrightarrow> D = inverse (sqrt x) / 2"