src/HOL/Lim.thy
 changeset 31017 2c227493ea56 parent 30273 ecd6f0ca62ea child 31336 e17f13cd1280
equal 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"`