src/HOL/Lim.thy
changeset 31017 2c227493ea56
parent 30273 ecd6f0ca62ea
child 31336 e17f13cd1280
equal deleted inserted replaced
31016:e1309df633c6 31017:2c227493ea56
   381 lemmas LIM_scaleR = scaleR.LIM
   381 lemmas LIM_scaleR = scaleR.LIM
   382 
   382 
   383 lemmas LIM_of_real = of_real.LIM
   383 lemmas LIM_of_real = of_real.LIM
   384 
   384 
   385 lemma LIM_power:
   385 lemma LIM_power:
   386   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::{recpower,real_normed_algebra}"
   386   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::{power,real_normed_algebra}"
   387   assumes f: "f -- a --> l"
   387   assumes f: "f -- a --> l"
   388   shows "(\<lambda>x. f x ^ n) -- a --> l ^ n"
   388   shows "(\<lambda>x. f x ^ n) -- a --> l ^ n"
   389 by (induct n, simp, simp add: LIM_mult f)
   389 by (induct n, simp, simp add: LIM_mult f)
   390 
   390 
   391 subsubsection {* Derived theorems about @{term LIM} *}
   391 subsubsection {* Derived theorems about @{term LIM} *}
   528 lemma isCont_of_real:
   528 lemma isCont_of_real:
   529   "isCont f a \<Longrightarrow> isCont (\<lambda>x. of_real (f x)) a"
   529   "isCont f a \<Longrightarrow> isCont (\<lambda>x. of_real (f x)) a"
   530   unfolding isCont_def by (rule LIM_of_real)
   530   unfolding isCont_def by (rule LIM_of_real)
   531 
   531 
   532 lemma isCont_power:
   532 lemma isCont_power:
   533   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::{recpower,real_normed_algebra}"
   533   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::{power,real_normed_algebra}"
   534   shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a"
   534   shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a"
   535   unfolding isCont_def by (rule LIM_power)
   535   unfolding isCont_def by (rule LIM_power)
   536 
   536 
   537 lemma isCont_sgn:
   537 lemma isCont_sgn:
   538   "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. sgn (f x)) a"
   538   "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. sgn (f x)) a"